diff options
author | 2012-10-04 13:32:50 -0700 | |
---|---|---|
committer | 2012-10-04 13:32:50 -0700 | |
commit | 8911e5c95d4715c2e2626aef67f19793d6f43201 (patch) | |
tree | d703bfd931802e780430e32f1339cf77adc342a4 /Source/Jennisys/examples/oopsla12/IntSet.jen | |
parent | 1c375d1889e628fcd2a1a0fc041673a5f4230d84 (diff) |
Put all sources under \Source directory
Diffstat (limited to 'Source/Jennisys/examples/oopsla12/IntSet.jen')
-rw-r--r-- | Source/Jennisys/examples/oopsla12/IntSet.jen | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/Source/Jennisys/examples/oopsla12/IntSet.jen b/Source/Jennisys/examples/oopsla12/IntSet.jen new file mode 100644 index 00000000..4800371e --- /dev/null +++ b/Source/Jennisys/examples/oopsla12/IntSet.jen @@ -0,0 +1,30 @@ +interface IntSet {
+ var elems: set[int]
+
+ constructor Singleton(x: int)
+ elems := {x}
+
+ constructor Dupleton(x: int, y: int)
+ requires x != y
+ elems := {x y}
+
+ method Find(x: int) returns (ret: bool)
+ ret := x in elems
+}
+
+datamodel IntSet {
+ var data: int
+ var left: IntSet
+ var right: IntSet
+
+ frame left * right
+
+ invariant
+ elems = {data} +
+ (left != null ? left.elems : {}) +
+ (right != null ? right.elems : {})
+ left != null ==>
+ (forall e :: e in left.elems ==> e < data)
+ right != null ==>
+ (forall e :: e in right.elems ==> data < e)
+}
\ No newline at end of file |