diff options
Diffstat (limited to 'Jennisys/Jennisys/examples/mod/jennisys-synth_Set.dfy')
| -rw-r--r-- | Jennisys/Jennisys/examples/mod/jennisys-synth_Set.dfy | 388 |
1 files changed, 0 insertions, 388 deletions
diff --git a/Jennisys/Jennisys/examples/mod/jennisys-synth_Set.dfy b/Jennisys/Jennisys/examples/mod/jennisys-synth_Set.dfy deleted file mode 100644 index 40404bfb..00000000 --- a/Jennisys/Jennisys/examples/mod/jennisys-synth_Set.dfy +++ /dev/null @@ -1,388 +0,0 @@ -class Set {
- ghost var Repr: set<object>;
- ghost var elems: set<int>;
-
- var root: SetNode;
-
- function Valid_repr(): bool
- reads *;
- {
- this in Repr &&
- null !in Repr &&
- (root != null ==> root in Repr && root.Repr <= Repr && this !in root.Repr)
- }
-
- function Valid_self(): bool
- reads *;
- {
- Valid_repr() &&
- (root == null ==> elems == {}) &&
- (root != null ==> elems == root.elems)
- }
-
- function Valid(): bool
- reads *;
- {
- this.Valid_self() &&
- (root != null ==> root.Valid())
- }
-
-
- method Double(p: int, q: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures elems == {p, q};
- {
- var gensym67 := new SetNode;
- gensym67._synth_Set_Double_gensym67(p, q);
- this.elems := {p, q};
- this.root := gensym67;
- // repr stuff
- this.Repr := {this} + this.root.Repr;
- }
-
-
- method Empty()
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures elems == {};
- {
- this.elems := {};
- this.root := null;
- // repr stuff
- this.Repr := {this};
- }
-
-
- method Singleton(t: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures elems == {t};
- {
- var gensym67 := new SetNode;
- gensym67._synth_Set_Singleton_gensym67(t);
- this.elems := {t};
- this.root := gensym67;
- // repr stuff
- this.Repr := {this} + this.root.Repr;
- }
-
-
- method Sum(p: int, q: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures elems == {p + q};
- {
- var gensym69 := new SetNode;
- gensym69._synth_Set_Sum_gensym69(p, q);
- this.elems := {p + q};
- this.root := gensym69;
- // repr stuff
- this.Repr := {this} + this.root.Repr;
- }
-
-}
-
-class SetNode {
- ghost var Repr: set<object>;
- ghost var elems: set<int>;
-
- var data: int;
- var left: SetNode;
- var right: SetNode;
-
- function Valid_repr(): bool
- reads *;
- {
- this in Repr &&
- null !in Repr &&
- (left != null ==> left in Repr && left.Repr <= Repr && this !in left.Repr) &&
- (right != null ==> right in Repr && right.Repr <= Repr && this !in right.Repr)
- }
-
- function Valid_self(): bool
- reads *;
- {
- Valid_repr() &&
- (elems == ({data} + (if left != null then left.elems else {})) + (if right != null then right.elems else {})) &&
- (left != null ==> (forall e :: e in left.elems ==> e < data)) &&
- (right != null ==> (forall e :: e in right.elems ==> e > data))
- }
-
- function Valid(): bool
- reads *;
- {
- this.Valid_self() &&
- (left != null ==> left.Valid_self()) &&
- (right != null ==> right.Valid_self()) &&
- (left != null && left.left != null ==> left.left.Valid_self()) &&
- (left != null && left.right != null ==> left.right.Valid_self()) &&
- (right != null && right.left != null ==> right.left.Valid_self()) &&
- (right != null && right.right != null ==> right.right.Valid_self())
- }
-
-
- method Double(p: int, q: int)
- modifies this;
- requires p != q;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures elems == {p, q};
- {
- if (q > p) {
- var gensym77 := new SetNode;
- gensym77._synth_SetNode_Double_gensym77(q);
- this.data := p;
- this.elems := {p, q};
- this.left := null;
- this.right := gensym77;
- // repr stuff
- this.Repr := {this} + this.right.Repr;
- } else {
- var gensym77 := new SetNode;
- gensym77._synth_SetNode_Double_gensym77(p);
- this.data := q;
- this.elems := {p, q};
- this.left := null;
- this.right := gensym77;
- // repr stuff
- this.Repr := {this} + this.right.Repr;
- }
- }
-
-
- method _synth_SetNode_Double_gensym77(q: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures elems == {q};
- {
- this.data := q;
- this.elems := {q};
- this.left := null;
- this.right := null;
- // repr stuff
- this.Repr := {this};
- }
-
-
- method _synth_SetNode_Triple_gensym80(r: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures elems == {r};
- {
- this.data := r;
- this.elems := {r};
- this.left := null;
- this.right := null;
- // repr stuff
- this.Repr := {this};
- }
-
-
- method Triple(p: int, q: int, r: int)
- modifies this;
- requires p != q;
- requires q != r;
- requires r != p;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures elems == {p, q, r};
- {
- if (p < q && r > q) {
- var gensym80 := new SetNode;
- var gensym81 := new SetNode;
- gensym80._synth_SetNode_Triple_gensym80(r);
- gensym81._synth_SetNode_Triple_gensym81(p);
- this.data := q;
- this.elems := {p, q, r};
- this.left := gensym81;
- this.right := gensym80;
- // repr stuff
- this.Repr := ({this} + this.left.Repr) + this.right.Repr;
- } else {
- if (r < p && q > p) {
- var gensym80 := new SetNode;
- var gensym81 := new SetNode;
- gensym80._synth_SetNode_Triple_gensym80(q);
- gensym81._synth_SetNode_Triple_gensym81(r);
- this.data := p;
- this.elems := {p, q, r};
- this.left := gensym81;
- this.right := gensym80;
- // repr stuff
- this.Repr := ({this} + this.left.Repr) + this.right.Repr;
- } else {
- if (p < r && q > r) {
- var gensym80 := new SetNode;
- var gensym81 := new SetNode;
- gensym80._synth_SetNode_Triple_gensym80(q);
- gensym81._synth_SetNode_Triple_gensym81(p);
- this.data := r;
- this.elems := {p, q, r};
- this.left := gensym81;
- this.right := gensym80;
- // repr stuff
- this.Repr := ({this} + this.left.Repr) + this.right.Repr;
- } else {
- if (r < q && p > q) {
- var gensym80 := new SetNode;
- var gensym81 := new SetNode;
- gensym80._synth_SetNode_Triple_gensym80(p);
- gensym81._synth_SetNode_Triple_gensym81(r);
- this.data := q;
- this.elems := {p, q, r};
- this.left := gensym81;
- this.right := gensym80;
- // repr stuff
- this.Repr := ({this} + this.left.Repr) + this.right.Repr;
- } else {
- if (q < r && p > r) {
- var gensym80 := new SetNode;
- var gensym81 := new SetNode;
- gensym80._synth_SetNode_Triple_gensym80(p);
- gensym81._synth_SetNode_Triple_gensym81(q);
- this.data := r;
- this.elems := {p, q, r};
- this.left := gensym81;
- this.right := gensym80;
- // repr stuff
- this.Repr := ({this} + this.left.Repr) + this.right.Repr;
- } else {
- var gensym80 := new SetNode;
- var gensym81 := new SetNode;
- gensym80._synth_SetNode_Triple_gensym80(r);
- gensym81._synth_SetNode_Triple_gensym81(q);
- this.data := p;
- this.elems := {p, q, r};
- this.left := gensym81;
- this.right := gensym80;
- // repr stuff
- this.Repr := ({this} + this.left.Repr) + this.right.Repr;
- }
- }
- }
- }
- }
- }
-
-
- method _synth_SetNode_Triple_gensym81(p: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures elems == {p};
- {
- this.data := p;
- this.elems := {p};
- this.left := null;
- this.right := null;
- // repr stuff
- this.Repr := {this};
- }
-
-
- method Init(t: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures elems == {t};
- {
- this.data := t;
- this.elems := {t};
- this.left := null;
- this.right := null;
- // repr stuff
- this.Repr := {this};
- }
-
-
- method _synth_SetNode__synth_Set_Double_gensym67_gensym77(q: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures elems == {q};
- {
- this.data := q;
- this.elems := {q};
- this.left := null;
- this.right := null;
- // repr stuff
- this.Repr := {this};
- }
-
-
- method _synth_Set_Double_gensym67(p: int, q: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures elems == {p, q};
- {
- if (q > p) {
- var gensym77 := new SetNode;
- gensym77._synth_SetNode__synth_Set_Double_gensym67_gensym77(q);
- this.data := p;
- this.elems := {p, q};
- this.left := null;
- this.right := gensym77;
- // repr stuff
- this.Repr := {this} + this.right.Repr;
- } else {
- if (p > q) {
- var gensym77 := new SetNode;
- gensym77._synth_SetNode__synth_Set_Double_gensym67_gensym77(p);
- this.data := q;
- this.elems := {p, q};
- this.left := null;
- this.right := gensym77;
- // repr stuff
- this.Repr := {this} + this.right.Repr;
- } else {
- this.data := q;
- this.elems := {p, q};
- this.left := null;
- this.right := null;
- // repr stuff
- this.Repr := {this};
- }
- }
- }
-
-
- method _synth_Set_Singleton_gensym67(t: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures elems == {t};
- {
- this.data := t;
- this.elems := {t};
- this.left := null;
- this.right := null;
- // repr stuff
- this.Repr := {this};
- }
-
-
- method _synth_Set_Sum_gensym69(p: int, q: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures elems == {p + q};
- {
- this.data := p + q;
- this.elems := {p + q};
- this.left := null;
- this.right := null;
- // repr stuff
- this.Repr := {this};
- }
-
-}
-
-
|