diff options
Diffstat (limited to 'Jennisys/Jennisys/examples/mod/jennisys-synth_List3.dfy')
| -rw-r--r-- | Jennisys/Jennisys/examples/mod/jennisys-synth_List3.dfy | 393 |
1 files changed, 0 insertions, 393 deletions
diff --git a/Jennisys/Jennisys/examples/mod/jennisys-synth_List3.dfy b/Jennisys/Jennisys/examples/mod/jennisys-synth_List3.dfy deleted file mode 100644 index e079b608..00000000 --- a/Jennisys/Jennisys/examples/mod/jennisys-synth_List3.dfy +++ /dev/null @@ -1,393 +0,0 @@ -class IntList {
- ghost var Repr: set<object>;
- ghost var list: seq<int>;
-
- var root: IntNode;
-
- 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 ==> |list| == 0) &&
- (root != null ==> |list| == |root.succ| + 1 && (list[0] == root.data && (forall i :: 1 <= i && i <= |root.succ| ==> root.succ[i - 1] != null && list[i] == root.succ[i - 1].data)))
- }
-
- 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 list == [p] + [q];
- {
- var gensym68 := new IntNode;
- gensym68._synth_IntList_Double_gensym68(p, q);
- this.list := [p] + [q];
- this.root := gensym68;
- // repr stuff
- this.Repr := {this} + this.root.Repr;
- }
-
-
- method Empty()
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures list == [];
- {
- this.list := [];
- this.root := null;
- // repr stuff
- this.Repr := {this};
- }
-
-
- method OneTwo()
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures list == [1, 2];
- {
- var gensym65 := new IntNode;
- gensym65._synth_IntList_OneTwo_gensym65();
- this.list := [1, 2];
- this.root := gensym65;
- // repr stuff
- this.Repr := {this} + this.root.Repr;
- }
-
-
- method Singleton(p: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures list == [p];
- {
- var gensym70 := new IntNode;
- gensym70._synth_IntList_Singleton_gensym70(p);
- this.list := [p];
- this.root := gensym70;
- // repr stuff
- this.Repr := {this} + this.root.Repr;
- }
-
-
- method SingletonTwo()
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures list == [2];
- {
- var gensym69 := new IntNode;
- gensym69._synth_IntList_SingletonTwo_gensym69();
- this.list := [2];
- this.root := gensym69;
- // repr stuff
- this.Repr := {this} + this.root.Repr;
- }
-
-
- method Sum(p: int, q: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures list == [p + q];
- {
- var gensym71 := new IntNode;
- gensym71._synth_IntList_Sum_gensym71(p, q);
- this.list := [p + q];
- this.root := gensym71;
- // repr stuff
- this.Repr := {this} + this.root.Repr;
- }
-
-
- method TwoConsecutive(p: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures list == [p] + [p + 1];
- {
- var gensym67 := new IntNode;
- gensym67._synth_IntList_TwoConsecutive_gensym67(p);
- this.list := [p] + [p + 1];
- this.root := gensym67;
- // repr stuff
- this.Repr := {this} + this.root.Repr;
- }
-
-}
-
-class IntNode {
- ghost var Repr: set<object>;
- ghost var succ: seq<IntNode>;
- ghost var data: int;
-
- var next: IntNode;
-
- function Valid_repr(): bool
- reads *;
- {
- this in Repr &&
- null !in Repr &&
- (next != null ==> next in Repr && next.Repr <= Repr && this !in next.Repr)
- }
-
- function Valid_self(): bool
- reads *;
- {
- Valid_repr() &&
- (next == null ==> |succ| == 0) &&
- (next != null ==> succ == [next] + next.succ) &&
- (!(null in succ))
- }
-
- function Valid(): bool
- reads *;
- {
- this.Valid_self() &&
- (next != null ==> next.Valid_self()) &&
- (next != null && next.next != null ==> next.next.Valid_self())
- }
-
-
- method Init(p: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures data == p;
- {
- this.data := p;
- this.next := null;
- this.succ := [];
- // repr stuff
- this.Repr := {this};
- }
-
-
- method InitInc(p: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures data == p + 1;
- {
- this.data := p + 1;
- this.next := null;
- this.succ := [];
- // repr stuff
- this.Repr := {this};
- }
-
-
- method Zero()
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures data == 0;
- ensures succ == [];
- {
- this.data := 0;
- this.next := null;
- this.succ := [];
- // repr stuff
- this.Repr := {this};
- }
-
-
- method _synth_IntList_Double_gensym68(p: int, q: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures data == p;
- ensures |succ| == 1;
- ensures succ[0].data == q;
- ensures succ[0].succ == [];
- {
- var gensym80 := new IntNode;
- gensym80._synth_IntNode__synth_IntList_Double_gensym68_gensym80(q);
- this.data := p;
- this.next := gensym80;
- this.succ := [gensym80];
- // repr stuff
- this.Repr := {this} + this.next.Repr;
- }
-
-
- method _synth_IntList_OneTwo_gensym65()
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures data == 1;
- ensures |succ| == 1;
- ensures succ[0].data == 2;
- ensures succ[0].succ == [];
- {
- var gensym78 := new IntNode;
- gensym78._synth_IntNode__synth_IntList_OneTwo_gensym65_gensym78();
- this.data := 1;
- this.next := gensym78;
- this.succ := [gensym78];
- // repr stuff
- this.Repr := {this} + this.next.Repr;
- }
-
-
- method _synth_IntList_SingletonTwo_gensym69()
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures data == 2;
- ensures |succ| == 0;
- {
- this.data := 2;
- this.next := null;
- this.succ := [];
- // repr stuff
- this.Repr := {this};
- }
-
-
- method _synth_IntList_Singleton_gensym70(p: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures data == p;
- ensures |succ| == 0;
- {
- this.data := p;
- this.next := null;
- this.succ := [];
- // repr stuff
- this.Repr := {this};
- }
-
-
- method _synth_IntList_Sum_gensym71(p: int, q: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures data == p + q;
- ensures |succ| == 0;
- {
- this.data := p + q;
- this.next := null;
- this.succ := [];
- // repr stuff
- this.Repr := {this};
- }
-
-
- method _synth_IntList_TwoConsecutive_gensym67(p: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures data == p;
- ensures |succ| == 1;
- ensures succ[0].data == p + 1;
- ensures succ[0].succ == [];
- {
- var gensym79 := new IntNode;
- gensym79._synth_IntNode__synth_IntList_TwoConsecutive_gensym67_gensym79(p);
- this.data := p;
- this.next := gensym79;
- this.succ := [gensym79];
- // repr stuff
- this.Repr := {this} + this.next.Repr;
- }
-
-
- method OneTwo()
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures data == 1;
- ensures |succ| == 1;
- ensures succ[0] != null;
- ensures succ[0].data == 2;
- {
- var gensym73 := new IntNode;
- gensym73._synth_IntNode_OneTwo_gensym73();
- this.data := 1;
- this.next := gensym73;
- this.succ := [gensym73];
- // repr stuff
- this.Repr := {this} + this.next.Repr;
- }
-
-
- method _synth_IntNode_OneTwo_gensym73()
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures data == 2;
- ensures |succ| == 0;
- {
- this.data := 2;
- this.next := null;
- this.succ := [];
- // repr stuff
- this.Repr := {this};
- }
-
-
- method _synth_IntNode__synth_IntList_Double_gensym68_gensym80(q: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures data == q;
- ensures |succ| == 0;
- {
- this.data := q;
- this.next := null;
- this.succ := [];
- // repr stuff
- this.Repr := {this};
- }
-
-
- method _synth_IntNode__synth_IntList_OneTwo_gensym65_gensym78()
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures data == 2;
- ensures |succ| == 0;
- {
- this.data := 2;
- this.next := null;
- this.succ := [];
- // repr stuff
- this.Repr := {this};
- }
-
-
- method _synth_IntNode__synth_IntList_TwoConsecutive_gensym67_gensym79(p: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures data == p + 1;
- ensures |succ| == 0;
- {
- this.data := p + 1;
- this.next := null;
- this.succ := [];
- // repr stuff
- this.Repr := {this};
- }
-
-}
-
-
|