diff options
Diffstat (limited to 'Test/dafny1/BinaryTree.dfy')
| -rw-r--r-- | Test/dafny1/BinaryTree.dfy | 243 |
1 files changed, 0 insertions, 243 deletions
diff --git a/Test/dafny1/BinaryTree.dfy b/Test/dafny1/BinaryTree.dfy deleted file mode 100644 index 88b06605..00000000 --- a/Test/dafny1/BinaryTree.dfy +++ /dev/null @@ -1,243 +0,0 @@ -class IntSet {
- ghost var Contents: set<int>;
- ghost var Repr: set<object>;
-
- var root: Node;
-
- function Valid(): bool
- reads this, Repr;
- {
- this in Repr &&
- (root == null ==> Contents == {}) &&
- (root != null ==>
- root in Repr && root.Repr <= Repr && this !in root.Repr &&
- root.Valid() &&
- Contents == root.Contents)
- }
-
- method Init()
- modifies this;
- ensures Valid() && fresh(Repr - {this});
- ensures Contents == {};
- {
- root := null;
- Repr := {this};
- Contents := {};
- }
-
- method Find(x: int) returns (present: bool)
- requires Valid();
- ensures present <==> x in Contents;
- {
- if (root == null) {
- present := false;
- } else {
- present := root.Find(x);
- }
- }
-
- method Insert(x: int)
- requires Valid();
- modifies Repr;
- ensures Valid() && fresh(Repr - old(Repr));
- ensures Contents == old(Contents) + {x};
- {
- var t := InsertHelper(x, root);
- root := t;
- Contents := root.Contents;
- Repr := root.Repr + {this};
- }
-
- static method InsertHelper(x: int, n: Node) returns (m: Node)
- requires n == null || n.Valid();
- modifies n.Repr;
- ensures m != null && m.Valid();
- ensures n == null ==> fresh(m.Repr) && m.Contents == {x};
- ensures n != null ==> m == n && n.Contents == old(n.Contents) + {x};
- ensures n != null ==> fresh(n.Repr - old(n.Repr));
- decreases if n == null then {} else n.Repr;
- {
- if (n == null) {
- m := new Node.Init(x);
- } else if (x == n.data) {
- m := n;
- } else {
- if (x < n.data) {
- assert n.right == null || n.right.Valid();
- var t := InsertHelper(x, n.left);
- n.left := t;
- n.Repr := n.Repr + n.left.Repr;
- } else {
- assert n.left == null || n.left.Valid();
- var t := InsertHelper(x, n.right);
- n.right := t;
- n.Repr := n.Repr + n.right.Repr;
- }
- n.Contents := n.Contents + {x};
- m := n;
- }
- }
-
- method Remove(x: int)
- requires Valid();
- modifies Repr;
- ensures Valid() && fresh(Repr - old(Repr));
- ensures Contents == old(Contents) - {x};
- {
- if (root != null) {
- var newRoot := root.Remove(x);
- root := newRoot;
- if (root == null) {
- Contents := {};
- Repr := {this};
- } else {
- Contents := root.Contents;
- Repr := root.Repr + {this};
- }
- }
- }
-}
-
-class Node {
- ghost var Contents: set<int>;
- ghost var Repr: set<object>;
-
- var data: int;
- var left: Node;
- var right: Node;
-
- function Valid(): bool
- reads this, Repr;
- {
- this in Repr &&
- null !in Repr &&
- (left != null ==>
- left in Repr &&
- left.Repr <= Repr && this !in left.Repr &&
- left.Valid() &&
- (forall y :: y in left.Contents ==> y < data)) &&
- (right != null ==>
- right in Repr &&
- right.Repr <= Repr && this !in right.Repr &&
- right.Valid() &&
- (forall y :: y in right.Contents ==> data < y)) &&
- (left == null && right == null ==>
- Contents == {data}) &&
- (left != null && right == null ==>
- Contents == left.Contents + {data}) &&
- (left == null && right != null ==>
- Contents == {data} + right.Contents) &&
- (left != null && right != null ==>
- left.Repr !! right.Repr &&
- Contents == left.Contents + {data} + right.Contents)
- }
-
- method Init(x: int)
- modifies this;
- ensures Valid() && fresh(Repr - {this});
- ensures Contents == {x};
- {
- data := x;
- left := null;
- right := null;
- Contents := {x};
- Repr := {this};
- }
-
- method Find(x: int) returns (present: bool)
- requires Valid();
- ensures present <==> x in Contents;
- decreases Repr;
- {
- if (x == data) {
- present := true;
- } else if (left != null && x < data) {
- present := left.Find(x);
- } else if (right != null && data < x) {
- present := right.Find(x);
- } else {
- present := false;
- }
- }
-
- method Remove(x: int) returns (node: Node)
- requires Valid();
- modifies Repr;
- ensures fresh(Repr - old(Repr));
- ensures node != null ==> node.Valid();
- ensures node == null ==> old(Contents) <= {x};
- ensures node != null ==> node.Repr <= Repr && node.Contents == old(Contents) - {x};
- decreases Repr;
- {
- node := this;
- if (left != null && x < data) {
- var t := left.Remove(x);
- left := t;
- Contents := Contents - {x};
- if (left != null) { Repr := Repr + left.Repr; }
- } else if (right != null && data < x) {
- var t := right.Remove(x);
- right := t;
- Contents := Contents - {x};
- if (right != null) { Repr := Repr + right.Repr; }
- } else if (x == data) {
- if (left == null && right == null) {
- node := null;
- } else if (left == null) {
- node := right;
- } else if (right == null) {
- node := left;
- } else {
- // rotate
- var min, r := right.RemoveMin();
- data := min; right := r;
- Contents := Contents - {x};
- if (right != null) { Repr := Repr + right.Repr; }
- }
- }
- }
-
- method RemoveMin() returns (min: int, node: Node)
- requires Valid();
- modifies Repr;
- ensures fresh(Repr - old(Repr));
- ensures node != null ==> node.Valid();
- ensures node == null ==> old(Contents) == {min};
- ensures node != null ==> node.Repr <= Repr && node.Contents == old(Contents) - {min};
- ensures min in old(Contents) && (forall x :: x in old(Contents) ==> min <= x);
- decreases Repr;
- {
- if (left == null) {
- min := data;
- node := right;
- } else {
- var t;
- min, t := left.RemoveMin();
- left := t;
- node := this;
- Contents := Contents - {min};
- if (left != null) { Repr := Repr + left.Repr; }
- }
- }
-}
-
-class Main {
- method Client0(x: int)
- {
- var s := new IntSet.Init();
-
- s.Insert(12);
- s.Insert(24);
- var present := s.Find(x);
- assert present <==> x == 12 || x == 24;
- }
-
- method Client1(s: IntSet, x: int)
- requires s != null && s.Valid();
- modifies s.Repr;
- {
- s.Insert(x);
- s.Insert(24);
- assert old(s.Contents) - {x,24} == s.Contents - {x,24};
- }
-}
|