diff options
| author |  Rustan Leino <unknown> | 2013-03-05 17:01:25 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-03-05 17:01:25 -0800 |
| commit | 9f7c11c0a12a9b802f23d613abeee91a2fb47743 (patch) | |
| tree | ff0c5ffd982094c5d03828f1332be03a4d66b4ea /Test/dafny1 | |
| parent | c819fabbb8da669952cb7e2e5937c73ff6dcfabe (diff) | |
Removed Dafny, Jennisys, Chalice, and BCT, which now live in different Codeplex repositories.
Diffstat (limited to 'Test/dafny1')
29 files changed, 0 insertions, 3935 deletions
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer deleted file mode 100644 index 06cac03b..00000000 --- a/Test/dafny1/Answer +++ /dev/null @@ -1,124 +0,0 @@ -
--------------------- Queue.dfy --------------------
-
-Dafny program verifier finished with 22 verified, 0 errors
-
--------------------- PriorityQueue.dfy --------------------
-
-Dafny program verifier finished with 24 verified, 0 errors
-
--------------------- ExtensibleArray.dfy --------------------
-
-Dafny program verifier finished with 11 verified, 0 errors
-
--------------------- ExtensibleArrayAuto.dfy --------------------
-
-Dafny program verifier finished with 11 verified, 0 errors
-
--------------------- BinaryTree.dfy --------------------
-
-Dafny program verifier finished with 24 verified, 0 errors
-
--------------------- UnboundedStack.dfy --------------------
-
-Dafny program verifier finished with 12 verified, 0 errors
-
--------------------- SeparationLogicList.dfy --------------------
-
-Dafny program verifier finished with 16 verified, 0 errors
-
--------------------- ListCopy.dfy --------------------
-
-Dafny program verifier finished with 4 verified, 0 errors
-
--------------------- ListReverse.dfy --------------------
-
-Dafny program verifier finished with 2 verified, 0 errors
-
--------------------- ListContents.dfy --------------------
-
-Dafny program verifier finished with 9 verified, 0 errors
-
--------------------- MatrixFun.dfy --------------------
-
-Dafny program verifier finished with 8 verified, 0 errors
-
--------------------- pow2.dfy --------------------
-
-Dafny program verifier finished with 8 verified, 0 errors
-
--------------------- SchorrWaite.dfy --------------------
-
-Dafny program verifier finished with 10 verified, 0 errors
-
--------------------- SchorrWaite-stages.dfy --------------------
-
-Dafny program verifier finished with 16 verified, 0 errors
-
--------------------- Cubes.dfy --------------------
-
-Dafny program verifier finished with 2 verified, 0 errors
-
--------------------- SumOfCubes.dfy --------------------
-
-Dafny program verifier finished with 17 verified, 0 errors
-
--------------------- FindZero.dfy --------------------
-
-Dafny program verifier finished with 8 verified, 0 errors
-
--------------------- TerminationDemos.dfy --------------------
-
-Dafny program verifier finished with 14 verified, 0 errors
-
--------------------- Substitution.dfy --------------------
-
-Dafny program verifier finished with 12 verified, 0 errors
-
--------------------- TreeDatatype.dfy --------------------
-
-Dafny program verifier finished with 10 verified, 0 errors
-
--------------------- KatzManna.dfy --------------------
-
-Dafny program verifier finished with 6 verified, 0 errors
-
--------------------- Induction.dfy --------------------
-
-Dafny program verifier finished with 33 verified, 0 errors
-
--------------------- Rippling.dfy --------------------
-
-Dafny program verifier finished with 141 verified, 0 errors
-
--------------------- MoreInduction.dfy --------------------
-MoreInduction.dfy(75,1): Error BP5003: A postcondition might not hold on this return path.
-MoreInduction.dfy(74,11): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon0
-MoreInduction.dfy(80,1): Error BP5003: A postcondition might not hold on this return path.
-MoreInduction.dfy(79,21): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon0
-MoreInduction.dfy(85,1): Error BP5003: A postcondition might not hold on this return path.
-MoreInduction.dfy(84,11): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon0
-MoreInduction.dfy(90,1): Error BP5003: A postcondition might not hold on this return path.
-MoreInduction.dfy(89,22): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon0
-
-Dafny program verifier finished with 15 verified, 4 errors
-
--------------------- Celebrity.dfy --------------------
-
-Dafny program verifier finished with 10 verified, 0 errors
-
--------------------- BDD.dfy --------------------
-
-Dafny program verifier finished with 5 verified, 0 errors
-
--------------------- UltraFilter.dfy --------------------
-
-Dafny program verifier finished with 19 verified, 0 errors
diff --git a/Test/dafny1/BDD.dfy b/Test/dafny1/BDD.dfy deleted file mode 100644 index 3b6e478c..00000000 --- a/Test/dafny1/BDD.dfy +++ /dev/null @@ -1,60 +0,0 @@ -
-
-module SimpleBDD
-{
- class BDDNode
- {
- static predicate bitfunc(f: map<seq<bool>, bool>, n: nat)
- {
- forall i:seq<bool> :: i in f <==> |i| == n
- }
- ghost var Contents: map<seq<bool>, bool>;
- ghost var Repr: set<object>;
- ghost var n: nat;
- var f: BDDNode, t: BDDNode;
- var b: bool;
- predicate valid()
- reads this, Repr;
- {
- bitfunc(Contents,n) &&
- (0 == n ==> (b <==> Contents[[]])) &&
- (0 < n ==> this in Repr && f != null && t != null && t in Repr && f in Repr && t.Repr <= Repr && f.Repr <= Repr && this !in f.Repr && this !in t.Repr && t.valid() && f.valid() &&
- t.n == f.n == n-1 &&
- (forall s | s in t.Contents :: Contents[[true] + s] <==> t.Contents[s]) &&
- (forall s | s in f.Contents :: Contents[[false] + s] <==> f.Contents[s]))
- }
- }
- class BDD
- {
- var root: BDDNode;
- predicate valid()
- reads this, Repr;
- {
- root != null && root in Repr && root.Repr <= Repr && root.valid() &&
- n == root.n && Contents == root.Contents
- }
-
- ghost var Contents: map<seq<bool>, bool>;
- var n: nat;
- ghost var Repr: set<object>;
-
- method Eval(s: seq<bool>) returns(b: bool)
- requires valid() && |s| == n;
- ensures b == Contents[s];
- {
- var node: BDDNode := root;
- var i := n;
- assert s[n-i..] == s;
- while(i > 0)
- invariant node != null && node.valid();
- invariant 0 <= i == node.n <= n;
- invariant Contents[s] == node.Contents[s[n-i..]];
- {
- assert s[n-i..] == [s[n-i]] + s[n-i+1..];
- node := if s[n-i] then node.t else node.f;
- i := i - 1;
- }
- b := node.b;
- }
- }
-}
\ No newline at end of file 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};
- }
-}
diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy deleted file mode 100644 index 4c761671..00000000 --- a/Test/dafny1/Celebrity.dfy +++ /dev/null @@ -1,90 +0,0 @@ -// Celebrity example, inspired by the Rodin tutorial
-
-static function method Knows<Person>(a: Person, b: Person): bool
- requires a != b; // forbid asking about the reflexive case
-
-static function IsCelebrity<Person>(c: Person, people: set<Person>): bool
-{
- c in people &&
- (forall p :: p in people && p != c ==> Knows(p, c) && !Knows(c, p))
-}
-
-method FindCelebrity0<Person>(people: set<Person>, ghost c: Person) returns (r: Person)
- requires exists c :: IsCelebrity(c, people);
- ensures r == c;
-{
- var cc; assume cc == c; // this line essentially converts ghost c to non-ghost cc
- r := cc;
-}
-
-method FindCelebrity1<Person>(people: set<Person>, ghost c: Person) returns (r: Person)
- requires IsCelebrity(c, people);
- ensures r == c;
-{
- var Q := people;
- var x := choose Q;
- while (Q != {x})
- //invariant Q <= people; // inv1 in Rodin's Celebrity_1, but it's not needed here
- invariant IsCelebrity(c, Q); // inv2
- invariant x in Q;
- decreases Q;
- {
- var y := choose Q - {x};
- if (Knows(x, y)) {
- Q := Q - {x}; // remove_1
- } else {
- Q := Q - {y}; assert x in Q; // remove_2
- }
- x := choose Q;
- }
- r := x;
-}
-
-method FindCelebrity2<Person>(people: set<Person>, ghost c: Person) returns (r: Person)
- requires IsCelebrity(c, people);
- ensures r == c;
-{
- var b := choose people;
- var R := people - {b};
- while (R != {})
- invariant R <= people; // inv1
- invariant b in people; // inv2
- invariant b !in R; // inv3
- invariant IsCelebrity(c, R + {b}); // my non-refinement way of saying inv4
-
- decreases R;
- {
- var x := choose R;
- if (Knows(x, b)) {
- R := R - {x};
- } else {
- b := x;
- R := R - {x};
- }
- }
- r := b;
-}
-
-method FindCelebrity3(n: int, people: set<int>, ghost c: int) returns (r: int)
- requires 0 < n;
- requires (forall p :: p in people <==> 0 <= p && p < n);
- requires IsCelebrity(c, people);
- ensures r == c;
-{
- r := 0;
- var a := 1;
- var b := 0;
- while (a < n)
- invariant a <= n;
- invariant b < a; // Celebrity_2/inv3 and Celebrity_3/inv2
- invariant c == b || (a <= c && c < n);
- {
- if (Knows(a, b)) {
- a := a + 1;
- } else {
- b := a;
- a := a + 1;
- }
- }
- r := b;
-}
diff --git a/Test/dafny1/Cubes.dfy b/Test/dafny1/Cubes.dfy deleted file mode 100644 index 1ada79fa..00000000 --- a/Test/dafny1/Cubes.dfy +++ /dev/null @@ -1,23 +0,0 @@ -method Cubes(a: array<int>)
- requires a != null;
- modifies a;
- ensures (forall i :: 0 <= i && i < a.Length ==> a[i] == i*i*i);
-{
- var n := 0;
- var c := 0;
- var k := 1;
- var m := 6;
- while (n < a.Length)
- invariant n <= a.Length;
- invariant (forall i :: 0 <= i && i < n ==> a[i] == i*i*i);
- invariant c == n*n*n;
- invariant k == 3*n*n + 3*n + 1;
- invariant m == 6*n + 6;
- {
- a[n] := c;
- c := c + k;
- k := k + m;
- m := m + 6;
- n := n + 1;
- }
-}
diff --git a/Test/dafny1/ExtensibleArray.dfy b/Test/dafny1/ExtensibleArray.dfy deleted file mode 100644 index 405f3e15..00000000 --- a/Test/dafny1/ExtensibleArray.dfy +++ /dev/null @@ -1,126 +0,0 @@ -class ExtensibleArray<T> {
- ghost var Contents: seq<T>;
- ghost var Repr: set<object>;
-
- var elements: array<T>;
- var more: ExtensibleArray<array<T>>;
- var length: int;
- var M: int; // shorthand for: if more == null then 0 else 256 * |more.Contents|
-
- function Valid(): bool
- reads this, Repr;
- {
- // shape of data structure
- this in Repr &&
- elements != null && elements.Length == 256 && elements in Repr &&
- (more != null ==>
- more in Repr && more.Repr <= Repr && this !in more.Repr && elements !in more.Repr &&
- more.Valid() &&
- |more.Contents| != 0 &&
- forall j :: 0 <= j && j < |more.Contents| ==>
- more.Contents[j] != null && more.Contents[j].Length == 256 &&
- more.Contents[j] in Repr && more.Contents[j] !in more.Repr &&
- more.Contents[j] != elements &&
- forall k :: 0 <= k && k < |more.Contents| && k != j ==> more.Contents[j] != more.Contents[k]) &&
-
- // length
- M == (if more == null then 0 else 256 * |more.Contents|) &&
- 0 <= length && length <= M + 256 &&
- (more != null ==> M < length) &&
-
- // Contents
- length == |Contents| &&
- (forall i :: 0 <= i && i < M ==> Contents[i] == more.Contents[i / 256][i % 256]) &&
- (forall i :: M <= i && i < length ==> Contents[i] == elements[i - M])
- }
-
- constructor Init()
- modifies this;
- ensures Valid() && fresh(Repr - {this});
- ensures Contents == [];
- {
- elements := new T[256];
- more := null;
- length := 0;
- M := 0;
-
- Contents := [];
- Repr := {this}; Repr := Repr + {elements};
- }
-
- method Get(i: int) returns (t: T)
- requires Valid();
- requires 0 <= i && i < |Contents|;
- ensures t == Contents[i];
- decreases Repr;
- {
- if (M <= i) {
- t := elements[i - M];
- } else {
- var arr := more.Get(i / 256);
- t := arr[i % 256];
- }
- }
-
- method Set(i: int, t: T)
- requires Valid();
- requires 0 <= i && i < |Contents|;
- modifies Repr;
- ensures Valid() && fresh(Repr - old(Repr));
- ensures Contents == old(Contents)[i := t];
- {
- if (M <= i) {
- elements[i - M] := t;
- } else {
- var arr := more.Get(i / 256);
- arr[i % 256] := t;
- }
- Contents := Contents[i := t];
- }
-
- method Append(t: T)
- requires Valid();
- modifies Repr;
- ensures Valid() && fresh(Repr - old(Repr));
- ensures Contents == old(Contents) + [t];
- decreases Repr;
- {
- if (length == 0 || length % 256 != 0) {
- // there is room in "elements"
- elements[length - M] := t;
- } else {
- if (more == null) {
- more := new ExtensibleArray<array<T>>.Init();
- Repr := Repr + {more} + more.Repr;
- }
- // "elements" is full, so move it into "more" and allocate a new array
- more.Append(elements);
- Repr := Repr + more.Repr;
- M := M + 256;
- elements := new T[256];
- Repr := Repr + {elements};
- elements[0] := t;
- }
- length := length + 1;
- Contents := Contents + [t];
- }
-}
-
-method Main() {
- var a := new ExtensibleArray<int>.Init();
- var n := 0;
- while (n < 256*256+600)
- invariant a.Valid() && fresh(a.Repr);
- invariant |a.Contents| == n;
- {
- a.Append(n);
- n := n + 1;
- }
- var k := a.Get(570); print k, "\n";
- k := a.Get(0); print k, "\n";
- k := a.Get(1000); print k, "\n";
- a.Set(1000, 23);
- k := a.Get(0); print k, "\n";
- k := a.Get(1000); print k, "\n";
- k := a.Get(66000); print k, "\n";
-}
diff --git a/Test/dafny1/ExtensibleArrayAuto.dfy b/Test/dafny1/ExtensibleArrayAuto.dfy deleted file mode 100644 index f7f97deb..00000000 --- a/Test/dafny1/ExtensibleArrayAuto.dfy +++ /dev/null @@ -1,113 +0,0 @@ -class {:autocontracts} ExtensibleArray<T> {
- ghost var Contents: seq<T>;
-
- var elements: array<T>;
- var more: ExtensibleArray<array<T>>;
- var length: int;
- var M: int; // shorthand for: if more == null then 0 else 256 * |more.Contents|
-
- function Valid(): bool
- {
- // shape of data structure
- elements != null && elements.Length == 256 &&
- (more != null ==>
- elements !in more.Repr &&
- more.Valid() &&
- |more.Contents| != 0 &&
- forall j :: 0 <= j && j < |more.Contents| ==>
- more.Contents[j] != null && more.Contents[j].Length == 256 &&
- more.Contents[j] in Repr && more.Contents[j] !in more.Repr &&
- more.Contents[j] != elements &&
- forall k :: 0 <= k && k < |more.Contents| && k != j ==> more.Contents[j] != more.Contents[k]) &&
-
- // length
- M == (if more == null then 0 else 256 * |more.Contents|) &&
- 0 <= length && length <= M + 256 &&
- (more != null ==> M < length) &&
-
- // Contents
- length == |Contents| &&
- (forall i :: 0 <= i && i < M ==> Contents[i] == more.Contents[i / 256][i % 256]) &&
- (forall i :: M <= i && i < length ==> Contents[i] == elements[i - M])
- }
-
- constructor Init()
- ensures Contents == [];
- {
- elements := new T[256];
- more := null;
- length := 0;
- M := 0;
-
- Contents := [];
- }
-
- method Get(i: int) returns (t: T)
- requires 0 <= i && i < |Contents|;
- ensures t == Contents[i];
- decreases Repr;
- {
- if (M <= i) {
- t := elements[i - M];
- } else {
- var arr := more.Get(i / 256);
- t := arr[i % 256];
- }
- }
-
- method Set(i: int, t: T)
- requires 0 <= i && i < |Contents|;
- ensures Contents == old(Contents)[i := t];
- {
- if (M <= i) {
- elements[i - M] := t;
- } else {
- var arr := more.Get(i / 256);
- arr[i % 256] := t;
- }
- Contents := Contents[i := t];
- }
-
- method Append(t: T)
- ensures Contents == old(Contents) + [t];
- decreases Repr;
- {
- if (length == 0 || length % 256 != 0) {
- // there is room in "elements"
- elements[length - M] := t;
- } else {
- if (more == null) {
- more := new ExtensibleArray<array<T>>.Init();
- Repr := Repr + {more} + more.Repr;
- }
- // "elements" is full, so move it into "more" and allocate a new array
- more.Append(elements);
- Repr := Repr + more.Repr;
- M := M + 256;
- elements := new T[256];
- Repr := Repr + {elements};
- elements[0] := t;
- }
- length := length + 1;
- Contents := Contents + [t];
- }
-}
-
-method Main() {
- var a := new ExtensibleArray<int>.Init();
- var n := 0;
- while (n < 256*256+600)
- invariant a.Valid() && fresh(a.Repr);
- invariant |a.Contents| == n;
- {
- a.Append(n);
- n := n + 1;
- }
- var k := a.Get(570); print k, "\n";
- k := a.Get(0); print k, "\n";
- k := a.Get(1000); print k, "\n";
- a.Set(1000, 23);
- k := a.Get(0); print k, "\n";
- k := a.Get(1000); print k, "\n";
- k := a.Get(66000); print k, "\n";
-}
diff --git a/Test/dafny1/FindZero.dfy b/Test/dafny1/FindZero.dfy deleted file mode 100644 index c92dd065..00000000 --- a/Test/dafny1/FindZero.dfy +++ /dev/null @@ -1,76 +0,0 @@ -method FindZero(a: array<int>) returns (r: int)
- requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];
- requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
- ensures 0 <= r ==> r < a.Length && a[r] == 0;
- ensures r < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != 0;
-{
- var n := 0;
- while (n < a.Length)
- invariant forall i :: 0 <= i < n && i < a.Length ==> a[i] != 0;
- {
- if (a[n] == 0) { r := n; return; }
- Lemma(a, n, a[n]);
- n := n + a[n];
- }
- r := -1;
-}
-
-ghost method Lemma(a: array<int>, k: int, m: int)
- requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];
- requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
- requires 0 <= k;
- requires k < a.Length ==> m <= a[k];
- ensures forall i :: k <= i < k+m && i < a.Length ==> a[i] != 0;
- decreases m;
-{
- if (0 < m && k < a.Length) {
- assert a[k] != 0;
- Lemma(a, k+1, m-1);
- }
-}
-
-// -----------------------------------------------------------------
-
-method FindZero_GhostLoop(a: array<int>) returns (r: int)
- requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];
- requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
- ensures 0 <= r ==> r < a.Length && a[r] == 0;
- ensures r < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != 0;
-{
- var n := 0;
- while (n < a.Length)
- invariant forall i :: 0 <= i < n && i < a.Length ==> a[i] != 0;
- {
- if (a[n] == 0) { return n; }
- ghost var m := n;
- while (m < n + a[n])
- invariant m <= n + a[n] && m < a.Length;
- invariant n + a[n] - m <= a[m];
- invariant forall i :: 0 <= i < m && i < a.Length ==> a[i] != 0;
- {
- m := m + 1;
- if (m == a.Length) { break; }
- }
- n := n + a[n];
- }
- return -1;
-}
-
-// -----------------------------------------------------------------
-
-method FindZero_Assert(a: array<int>) returns (r: int)
- requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];
- requires forall i :: 0 <= i-1 && i < a.Length ==> a[i-1]-1 <= a[i];
- ensures 0 <= r ==> r < a.Length && a[r] == 0;
- ensures r < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != 0;
-{
- var n := 0;
- while (n < a.Length)
- invariant forall i :: 0 <= i < n && i < a.Length ==> a[i] != 0;
- {
- if (a[n] == 0) { return n; }
- assert forall m {:induction} :: n <= m < n + a[n] && m < a.Length ==> n+a[n]-m <= a[m];
- n := n + a[n];
- }
- return -1;
-}
diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy deleted file mode 100644 index 3585dde6..00000000 --- a/Test/dafny1/Induction.dfy +++ /dev/null @@ -1,202 +0,0 @@ -class IntegerInduction {
- // This class considers different ways of proving, for any natural n:
- // (SUM i in [0, n] :: i^3) == (SUM i in [0, n] :: i)^2
-
- // In terms of Dafny functions, the theorem to be proved is:
- // SumOfCubes(n) == Gauss(n) * Gauss(n)
-
- function SumOfCubes(n: int): int
- requires 0 <= n;
- {
- if n == 0 then 0 else SumOfCubes(n-1) + n*n*n
- }
-
- function Gauss(n: int): int
- requires 0 <= n;
- {
- if n == 0 then 0 else Gauss(n-1) + n
- }
-
- // Here is one proof. It uses a lemma, which is proved separately.
-
- ghost method Theorem0(n: int)
- requires 0 <= n;
- ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
- {
- if (n != 0) {
- Theorem0(n-1);
- Lemma(n-1);
- }
- }
-
- ghost method Lemma(n: int)
- requires 0 <= n;
- ensures 2 * Gauss(n) == n*(n+1);
- {
- if (n != 0) { Lemma(n-1); }
- }
-
- // Here is another proof. It states the lemma as part of the theorem, and
- // thus proves the two together.
-
- ghost method Theorem1(n: int)
- requires 0 <= n;
- ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
- ensures 2 * Gauss(n) == n*(n+1);
- {
- if (n != 0) {
- Theorem1(n-1);
- }
- }
-
- ghost method DoItAllInOneGo()
- ensures (forall n :: 0 <= n ==>
- SumOfCubes(n) == Gauss(n) * Gauss(n) &&
- 2 * Gauss(n) == n*(n+1));
- {
- }
-
- // The following two ghost methods are the same as the previous two, but
- // here no body is given--and the proof still goes through (thanks to
- // Dafny's ghost-method induction tactic).
-
- ghost method Lemma_Auto(n: int)
- requires 0 <= n;
- ensures 2 * Gauss(n) == n*(n+1);
- {
- }
-
- ghost method Theorem1_Auto(n: int)
- requires 0 <= n;
- ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
- ensures 2 * Gauss(n) == n*(n+1);
- {
- }
-
- // Here is another proof. It makes use of Dafny's induction heuristics to
- // prove the lemma.
-
- ghost method Theorem2(n: int)
- requires 0 <= n;
- ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
- {
- if (n != 0) {
- Theorem2(n-1);
-
- assert (forall m :: 0 <= m ==> 2 * Gauss(m) == m*(m+1));
- }
- }
-
- ghost method M(n: int)
- requires 0 <= n;
- {
- assume (forall k :: 0 <= k && k < n ==> 2 * Gauss(k) == k*(k+1)); // manually assume the induction hypothesis
- assert 2 * Gauss(n) == n*(n+1);
- }
-
- // Another way to prove the lemma is to supply a postcondition on the Gauss function
-
- ghost method Theorem3(n: int)
- requires 0 <= n;
- ensures SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n);
- {
- if (n != 0) {
- Theorem3(n-1);
- }
- }
-
- function GaussWithPost(n: int): int
- requires 0 <= n;
- ensures 2 * GaussWithPost(n) == n*(n+1);
- {
- if n == 0 then 0 else GaussWithPost(n-1) + n
- }
-
- // Finally, with the postcondition of GaussWithPost, one can prove the entire theorem by induction
-
- ghost method Theorem4()
- ensures (forall n :: 0 <= n ==>
- SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n));
- {
- // look ma, no hints!
- }
-
- ghost method Theorem5(n: int)
- requires 0 <= n;
- ensures SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n);
- {
- // the postcondition is a simple consequence of these quantified versions of the theorem:
- if (*) {
- assert (forall m :: 0 <= m ==> SumOfCubes(m) == GaussWithPost(m) * GaussWithPost(m));
- } else {
- Theorem4();
- }
- }
-
- // The body of this function method gives a single quantifier, which leads to an efficient
- // way to check sortedness at run time. However, an alternative, and ostensibly more general,
- // way to express sortedness is given in the function's postcondition. The alternative
- // formulation may be easier to understand for a human and may also be more readily applicable
- // for the program verifier. Dafny will show that postcondition holds, which ensures the
- // equivalence of the two formulations.
- // The proof of the postcondition requires induction. It would have been nicer to state it
- // as one formula of the form "IsSorted(s) <==> ...", but then Dafny would never consider the
- // possibility of applying induction. Instead, the "==>" and "<==" cases are given separately.
- // Proving the "<==" case is simple; it's the "==>" case that requires induction.
- // The example uses an attribute that requests induction on just "j". However, the proof also
- // goes through by applying induction on both bound variables.
- function method IsSorted(s: seq<int>): bool
- ensures IsSorted(s) ==> (forall i,j {:induction j} :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]);
- ensures (forall i,j :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]) ==> IsSorted(s);
- {
- (forall i :: 1 <= i && i < |s| ==> s[i-1] <= s[i])
- }
-}
-
-datatype Tree<T> = Leaf(T) | Branch(Tree<T>, Tree<T>);
-
-class DatatypeInduction<T> {
- function LeafCount<T>(tree: Tree<T>): int
- {
- match tree
- case Leaf(t) => 1
- case Branch(left, right) => LeafCount(left) + LeafCount(right)
- }
-
- method Theorem0(tree: Tree<T>)
- ensures 1 <= LeafCount(tree);
- {
- assert (forall t: Tree<T> :: 1 <= LeafCount(t));
- }
-
- // see also Test/dafny0/DTypes.dfy for more variations of this example
-
- function OccurrenceCount<T>(tree: Tree<T>, x: T): int
- {
- match tree
- case Leaf(t) => if x == t then 1 else 0
- case Branch(left, right) => OccurrenceCount(left, x) + OccurrenceCount(right, x)
- }
- method RegressionTest(tree: Tree<T>)
- // the translation of the following line once crashed Dafny
- requires forall y :: 0 <= OccurrenceCount(tree, y);
- {
- }
-
-}
-
-// ----------------------- Induction and case splits -----------------
-// This is a simple example where the induction hypothesis and the
-// case splits are decoupled.
-
-datatype D = Nothing | Something(D);
-
-function FooD(n: nat, d: D): int
- ensures 10 <= FooD(n, d);
-{
- match d
- case Nothing =>
- if n == 0 then 10 else FooD(n-1, D.Something(d))
- case Something(next) =>
- if n < 100 then n + 12 else FooD(n-13, next)
-}
diff --git a/Test/dafny1/KatzManna.dfy b/Test/dafny1/KatzManna.dfy deleted file mode 100644 index 38b2963e..00000000 --- a/Test/dafny1/KatzManna.dfy +++ /dev/null @@ -1,76 +0,0 @@ -method NinetyOne(x: int) returns (z: int)
- requires 0 <= x;
-// ensures z == (if x > 101 then x-10 else 91);
-{
- var y1 := x;
- var y2 := 1;
- while (true)
- invariant (y1 <= 111 && y2 >= 1) || (y1 == x && y2 == 1);
- decreases -2*y1 + 21*y2 + 2*(if x < 111 then 111 else x);
- {
- if (y1 > 100) {
- if (y2 == 1) {
- break;
- } else {
- y1 := y1 - 10;
- y2 := y2 - 1;
- }
- } else {
- y1 := y1 + 11;
- y2 := y2 + 1;
- }
- }
- z := y1 - 10;
-}
-
-method Gcd(x1: int, x2: int)
- requires 1 <= x1 && 1 <= x2;
-{
- var y1 := x1;
- var y2 := x2;
- while (y1 != y2)
- invariant 1 <= y1 && 1 <= y2;
- decreases y1 + y2;
- {
- while (y1 > y2)
- invariant 1 <= y1 && 1 <= y2;
- {
- y1 := y1 - y2;
- }
- while (y2 > y1)
- invariant 1 <= y1 && 1 <= y2;
- {
- y2 := y2 - y1;
- }
- }
-}
-
-method Determinant(X: array2<int>, M: int) returns (z: int)
- requires 1 <= M;
- requires X != null && M == X.Length0 && M == X.Length1;
- modifies X;
-{
- var y := X[1-1,1-1];
- var a := 1;
- while (a != M)
- invariant 1 <= a && a <= M;
- {
- var b := a + 1;
- while (b != M+1)
- invariant a+1 <= b && b <= M+1;
- {
- var c := M;
- while (c != a)
- invariant a <= c && c <= M;
- {
- assume X[a-1,a-1] != 0;
- X[b-1, c-1] := X[b-1,c-1] - X[b-1,a-1] / X[a-1,a-1] * X[a-1,c-1];
- c := c - 1;
- }
- b := b + 1;
- }
- a := a + 1;
- y := y * X[a-1,a-1];
- }
- z := y;
-}
diff --git a/Test/dafny1/ListContents.dfy b/Test/dafny1/ListContents.dfy deleted file mode 100644 index a8b4861d..00000000 --- a/Test/dafny1/ListContents.dfy +++ /dev/null @@ -1,91 +0,0 @@ -class Node<T> {
- var list: seq<T>;
- var footprint: set<Node<T>>;
-
- var data: T;
- var next: Node<T>;
-
- function Valid(): bool
- reads this, footprint;
- {
- this in this.footprint && null !in this.footprint &&
- (next == null ==> list == [data]) &&
- (next != null ==>
- next in footprint && next.footprint <= footprint &&
- this !in next.footprint &&
- list == [data] + next.list &&
- next.Valid())
- }
-
- method Init(d: T)
- modifies this;
- ensures Valid() && fresh(footprint - {this});
- ensures list == [d];
- {
- data := d;
- next := null;
- list := [d];
- footprint := {this};
- }
-
- method SkipHead() returns (r: Node<T>)
- requires Valid();
- ensures r == null ==> |list| == 1;
- ensures r != null ==> r.Valid() && r.footprint <= footprint;
- ensures r != null ==> r.list == list[1..];
- {
- r := next;
- }
-
- method Prepend(d: T) returns (r: Node<T>)
- requires Valid();
- ensures r != null && r.Valid() && fresh(r.footprint - old(footprint));
- ensures r.list == [d] + list;
- {
- r := new Node<T>;
- r.data := d;
- r.next := this;
- r.footprint := {r} + this.footprint;
- r.list := [r.data] + this.list;
- }
-
- method ReverseInPlace() returns (reverse: Node<T>)
- requires Valid();
- modifies footprint;
- ensures reverse != null && reverse.Valid();
- ensures fresh(reverse.footprint - old(footprint));
- ensures |reverse.list| == |old(list)|;
- ensures (forall i :: 0 <= i && i < |old(list)| ==> old(list)[i] == reverse.list[|old(list)|-1-i]);
- {
- var current := next;
- reverse := this;
- reverse.next := null;
- reverse.footprint := {reverse};
- reverse.list := [data];
-
- while (current != null)
- invariant reverse != null && reverse.Valid();
- invariant reverse.footprint <= old(footprint);
- invariant current == null ==> |old(list)| == |reverse.list|;
- invariant current != null ==>
- current.Valid() &&
- current in old(footprint) && current.footprint <= old(footprint) &&
- current.footprint !! reverse.footprint &&
- |old(list)| == |reverse.list| + |current.list|;
- invariant current != null ==> current.list == old(list)[|reverse.list|..];
- invariant
- (forall i :: 0 <= i && i < |reverse.list| ==> old(list)[i] == reverse.list[|reverse.list|-1-i]);
- decreases if current != null then |current.list| else -1;
- {
- var nx := current.next;
-
- // ..., reverse, current, nx, ...
- current.next := reverse;
- current.footprint := {current} + reverse.footprint;
- current.list := [current.data] + reverse.list;
-
- reverse := current;
- current := nx;
- }
- }
-}
diff --git a/Test/dafny1/ListCopy.dfy b/Test/dafny1/ListCopy.dfy deleted file mode 100644 index d5febfe0..00000000 --- a/Test/dafny1/ListCopy.dfy +++ /dev/null @@ -1,53 +0,0 @@ -class Node {
- var nxt: Node;
-
- method Init()
- modifies this;
- ensures nxt == null;
- {
- nxt := null;
- }
-
- method Copy(root: Node) returns (result: Node)
- {
- var existingRegion: set<Node>;
- assume root == null || root in existingRegion;
- assume (forall o: Node :: o != null && o in existingRegion && o.nxt != null ==> o.nxt in existingRegion);
-
- var newRoot := null;
- var oldListPtr := root;
- var newRegion: set<Node> := {};
-
- if (oldListPtr != null) {
- newRoot := new Node.Init();
- newRegion := newRegion + {newRoot};
- var prev := newRoot;
-
- while (oldListPtr != null)
- invariant newRoot in newRegion;
- invariant (forall o: Node :: o in newRegion ==> o != null);
- invariant (forall o: Node :: o in newRegion && o.nxt != null ==> o.nxt in newRegion);
- invariant prev in newRegion;
- invariant fresh(newRegion);
- invariant newRegion !! existingRegion;
- decreases *; // omit loop termination check
- {
- var tmp := new Node.Init();
-
- newRegion := newRegion + {tmp};
- prev.nxt := tmp;
-
- prev := tmp;
- oldListPtr := oldListPtr.nxt;
- }
- }
- result := newRoot;
- assert result == null || result in newRegion;
-
- // everything in newRegion is fresh
- assert fresh(newRegion);
-
- // newRegion # exisitingRegion
- assert newRegion !! existingRegion;
- }
-}
diff --git a/Test/dafny1/ListReverse.dfy b/Test/dafny1/ListReverse.dfy deleted file mode 100644 index ef029b88..00000000 --- a/Test/dafny1/ListReverse.dfy +++ /dev/null @@ -1,27 +0,0 @@ -
-class Node {
- var nxt: Node;
-
- method ReverseInPlace(x: Node, r: set<Node>) returns (reverse: Node)
- requires null !in r;
- requires x == null || x in r;
- requires (forall y :: y in r ==> y.nxt == null || y.nxt in r); // region closure
- modifies r;
- ensures reverse == null || reverse in r;
- ensures (forall y :: y in r ==> y.nxt == null || y.nxt in r); // region closure
- {
- var current := x;
- reverse := null;
- while (current != null)
- invariant current == null || current in r;
- invariant reverse == null || reverse in r;
- invariant (forall y :: y in r ==> y.nxt == null || y.nxt in r); // region closure
- decreases *; // omit loop termination check
- {
- var tmp := current.nxt;
- current.nxt := reverse;
- reverse := current;
- current := tmp;
- }
- }
-}
diff --git a/Test/dafny1/MatrixFun.dfy b/Test/dafny1/MatrixFun.dfy deleted file mode 100644 index 8f9d87ed..00000000 --- a/Test/dafny1/MatrixFun.dfy +++ /dev/null @@ -1,98 +0,0 @@ -method MirrorImage<T>(m: array2<T>)
- requires m != null;
- modifies m;
- ensures (forall i,j :: 0 <= i && i < m.Length0 && 0 <= j && j < m.Length1 ==>
- m[i,j] == old(m[i, m.Length1-1-j]));
-{
- var a := 0;
- while (a < m.Length0)
- invariant a <= m.Length0;
- invariant (forall i,j :: 0 <= i && i < a && 0 <= j && j < m.Length1 ==>
- m[i,j] == old(m[i, m.Length1-1-j]));
- invariant (forall i,j :: a <= i && i < m.Length0 && 0 <= j && j < m.Length1 ==>
- m[i,j] == old(m[i,j]));
- {
- var b := 0;
- while (b < m.Length1 / 2)
- invariant b <= m.Length1 / 2;
- invariant (forall i,j :: 0 <= i && i < a && 0 <= j && j < m.Length1 ==>
- m[i,j] == old(m[i, m.Length1-1-j]));
- invariant (forall j :: 0 <= j && j < b ==>
- m[a,j] == old(m[a, m.Length1-1-j]) &&
- old(m[a,j]) == m[a, m.Length1-1-j]);
- invariant (forall j :: b <= j && j < m.Length1-b ==> m[a,j] == old(m[a,j]));
- invariant (forall i,j :: a+1 <= i && i < m.Length0 && 0 <= j && j < m.Length1 ==>
- m[i,j] == old(m[i,j]));
- {
- m[a, m.Length1-1-b], m[a, b] := m[a, b], m[a, m.Length1-1-b];
- b := b + 1;
- }
- a := a + 1;
- }
-}
-
-method Flip<T>(m: array2<T>)
- requires m != null && m.Length0 == m.Length1;
- modifies m;
- ensures (forall i,j :: 0 <= i < m.Length0 && 0 <= j < m.Length1 ==> m[i,j] == old(m[j,i]));
-{
- var N := m.Length0;
- var a := 0;
- var b := 1;
- while (a != N)
- invariant a < b <= N || (a == N && b == N+1);
- invariant (forall i,j :: 0 <= i <= j < N ==>
- (if i < a || (i == a && j < b)
- then m[i,j] == old(m[j,i]) && m[j,i] == old(m[i,j])
- else m[i,j] == old(m[i,j]) && m[j,i] == old(m[j,i])));
- decreases N-a, N-b;
- {
- if (b < N) {
- m[a,b], m[b,a] := m[b,a], m[a,b];
- b := b + 1;
- } else {
- a := a + 1; b := a + 1;
- }
- }
-}
-
-method Main()
-{
- var B := new bool[2,5];
- B[0,0] := true; B[0,1] := false; B[0,2] := false; B[0,3] := true; B[0,4] := false;
- B[1,0] := true; B[1,1] := true; B[1,2] := true; B[1,3] := true; B[1,4] := false;
- print "Before:\n";
- PrintMatrix(B);
- MirrorImage(B);
- print "Mirror image:\n";
- PrintMatrix(B);
-
- var A := new int[3,3];
- A[0,0] := 5; A[0,1] := 7; A[0,2] := 9;
- A[1,0] := 6; A[1,1] := 2; A[1,2] := 3;
- A[2,0] := 7; A[2,1] := 1; A[2,2] := 0;
- print "Before:\n";
- PrintMatrix(A);
- Flip(A);
- print "Flip:\n";
- PrintMatrix(A);
-}
-
-method PrintMatrix<T>(m: array2<T>)
- requires m != null;
-{
- var i := 0;
- while (i < m.Length0) {
- var j := 0;
- while (j < m.Length1) {
- print m[i,j];
- j := j + 1;
- if (j == m.Length1) {
- print "\n";
- } else {
- print ", ";
- }
- }
- i := i + 1;
- }
-}
diff --git a/Test/dafny1/MoreInduction.dfy b/Test/dafny1/MoreInduction.dfy deleted file mode 100644 index 84c32fb3..00000000 --- a/Test/dafny1/MoreInduction.dfy +++ /dev/null @@ -1,97 +0,0 @@ -datatype List<X> = Nil | Cons(Node<X>, List<X>);
-datatype Node<X> = Element(X) | Nary(List<X>);
-
-function FlattenMain<X>(list: List<X>): List<X>
- ensures IsFlat(FlattenMain(list));
-{
- Flatten(list, Nil)
-}
-
-function Flatten<X>(list: List<X>, ext: List<X>): List<X>
- requires IsFlat(ext);
- ensures IsFlat(Flatten(list, ext));
-{
- match list
- case Nil => ext
- case Cons(n, rest) =>
- match n
- case Element(x) => Cons(n, Flatten(rest, ext))
- case Nary(nn) => Flatten(nn, Flatten(rest, ext))
-}
-
-function IsFlat<X>(list: List<X>): bool
-{
- match list
- case Nil => true
- case Cons(n, rest) =>
- match n
- case Element(x) => IsFlat(rest)
- case Nary(nn) => false
-}
-
-function ToSeq<X>(list: List<X>): seq<X>
-{
- match list
- case Nil => []
- case Cons(n, rest) =>
- match n
- case Element(x) => [x] + ToSeq(rest)
- case Nary(nn) => ToSeq(nn) + ToSeq(rest)
-}
-
-ghost method Theorem<X>(list: List<X>)
- ensures ToSeq(list) == ToSeq(FlattenMain(list));
-{
- Lemma(list, Nil);
-}
-
-ghost method Lemma<X>(list: List<X>, ext: List<X>)
- requires IsFlat(ext);
- ensures ToSeq(list) + ToSeq(ext) == ToSeq(Flatten(list, ext));
-{
- match (list) {
- case Nil =>
- case Cons(n, rest) =>
- match (n) {
- case Element(x) =>
- Lemma(rest, ext);
- case Nary(nn) =>
- Lemma(nn, Flatten(rest, ext));
- Lemma(rest, ext);
- }
- }
-}
-
-// ---------------------------------------------
-
-function NegFac(n: int): int
- decreases -n;
-{
- if -1 <= n then -1 else - NegFac(n+1) * n
-}
-
-ghost method LemmaAll()
- ensures forall n :: NegFac(n) <= -1; // error: induction heuristic does not give a useful well-founded order, and thus this fails to verify
-{
-}
-
-ghost method LemmaOne(n: int)
- ensures NegFac(n) <= -1; // error: induction heuristic does not give a useful well-founded order, and thus this fails to verify
-{
-}
-
-ghost method LemmaAll_Neg()
- ensures forall n :: NegFac(-n) <= -1; // error: fails to verify because of the minus in the trigger
-{
-}
-
-ghost method LemmaOne_Neg(n: int)
- ensures NegFac(-n) <= -1; // error: fails to verify because of the minus in the trigger
-{
-}
-
-ghost method LemmaOneWithDecreases(n: int)
- ensures NegFac(n) <= -1; // here, the programmer gives a good well-founded order, so this verifies
- decreases -n;
-{
-}
diff --git a/Test/dafny1/PriorityQueue.dfy b/Test/dafny1/PriorityQueue.dfy deleted file mode 100644 index 0343cb07..00000000 --- a/Test/dafny1/PriorityQueue.dfy +++ /dev/null @@ -1,221 +0,0 @@ -class PriorityQueue {
- var N: int; // capacity
- var n: int; // current size
- ghost var Repr: set<object>; // set of objects that make up the representation of a PriorityQueue
-
- var a: array<int>; // private implementation of PriorityQueue
-
- predicate Valid
- reads this, Repr;
- {
- MostlyValid &&
- (forall j :: 2 <= j && j <= n ==> a[j/2] <= a[j])
- }
-
- predicate MostlyValid
- reads this, Repr;
- {
- this in Repr && a in Repr &&
- a != null && a.Length == N+1 &&
- 0 <= n && n <= N
- }
-
- method Init(capacity: int)
- requires 0 <= capacity;
- modifies this;
- ensures Valid && fresh(Repr - {this});
- ensures N == capacity;
- {
- N := capacity;
- a := new int[N+1];
- n := 0;
- Repr := {this};
- Repr := Repr + {a};
- }
-
- method Insert(x: int)
- requires Valid && n < N;
- modifies this, a;
- ensures Valid && fresh(Repr - old(Repr));
- ensures n == old(n) + 1 && N == old(N);
- {
- n := n + 1;
- a[n] := x;
- SiftUp(n);
- }
-
- method SiftUp(k: int)
- requires 1 <= k && k <= n;
- requires MostlyValid;
- requires (forall j :: 2 <= j && j <= n && j != k ==> a[j/2] <= a[j]);
- requires (forall j :: 1 <= j && j <= n ==> j/2 != k); // k is a leaf
- modifies a;
- ensures Valid;
- {
- var i := k;
- assert MostlyValid;
- while (1 < i)
- invariant i <= k && MostlyValid;
- invariant (forall j :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]);
- invariant (forall j :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);
- {
- if (a[i/2] <= a[i]) {
- return;
- }
- a[i/2], a[i] := a[i], a[i/2];
- i := i / 2;
- }
- }
-
- method RemoveMin() returns (x: int)
- requires Valid && 1 <= n;
- modifies this, a;
- ensures Valid && fresh(Repr - old(Repr));
- ensures n == old(n) - 1;
- {
- x := a[1];
- a[1] := a[n];
- n := n - 1;
- SiftDown(1);
- }
-
- method SiftDown(k: int)
- requires 1 <= k;
- requires MostlyValid;
- requires (forall j :: 2 <= j && j <= n && j/2 != k ==> a[j/2] <= a[j]);
- requires (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != k ==> a[j/2/2] <= a[j]);
- // Alternatively, the line above can be expressed as:
- // requires (forall j :: 1 <= k/2 && j/2 == k && j <= n ==> a[j/2/2] <= a[j]);
- modifies a;
- ensures Valid;
- {
- var i := k;
- while (2*i <= n) // while i is not a leaf
- invariant 1 <= i && MostlyValid;
- invariant (forall j :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]);
- invariant (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != i ==> a[j/2/2] <= a[j]);
- {
- var smallestChild;
- if (2*i + 1 <= n && a[2*i + 1] < a[2*i]) {
- smallestChild := 2*i + 1;
- } else {
- smallestChild := 2*i;
- }
- if (a[i] <= a[smallestChild]) {
- return;
- }
- a[smallestChild], a[i] := a[i], a[smallestChild];
- i := smallestChild;
- assert 1 <= i/2/2 ==> a[i/2/2] <= a[i];
- }
- }
-}
-
-// ---------- Alternative specifications ----------
-
-class PriorityQueue_Alternative {
- var N: int; // capacity
- var n: int; // current size
- ghost var Repr: set<object>; // set of objects that make up the representation of a PriorityQueue
-
- var a: array<int>; // private implementation of PriorityQueue
-
- predicate Valid
- reads this, Repr;
- {
- MostlyValid &&
- (forall j :: 2 <= j && j <= n ==> a[j/2] <= a[j])
- }
-
- predicate MostlyValid
- reads this, Repr;
- {
- this in Repr && a in Repr &&
- a != null && a.Length == N+1 &&
- 0 <= n && n <= N
- }
-
- method Init(capacity: int)
- requires 0 <= capacity;
- modifies this;
- ensures Valid && fresh(Repr - {this});
- ensures N == capacity;
- {
- N := capacity;
- a := new int[N+1];
- n := 0;
- Repr := {this};
- Repr := Repr + {a};
- }
-
- method Insert(x: int)
- requires Valid && n < N;
- modifies this, a;
- ensures Valid && fresh(Repr - old(Repr));
- ensures n == old(n) + 1 && N == old(N);
- {
- n := n + 1;
- a[n] := x;
- SiftUp();
- }
-
- method SiftUp()
- requires MostlyValid;
- requires (forall j :: 2 <= j && j <= n && j != n ==> a[j/2] <= a[j]);
- modifies a;
- ensures Valid;
- {
- var i := n;
- assert MostlyValid;
- while (1 < i)
- invariant i <= n && MostlyValid;
- invariant (forall j :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]);
- invariant (forall j :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);
- {
- if (a[i/2] <= a[i]) {
- return;
- }
- a[i/2], a[i] := a[i], a[i/2];
- i := i / 2;
- }
- }
-
- method RemoveMin() returns (x: int)
- requires Valid && 1 <= n;
- modifies this, a;
- ensures Valid && fresh(Repr - old(Repr));
- ensures n == old(n) - 1;
- {
- x := a[1];
- a[1] := a[n];
- n := n - 1;
- SiftDown();
- }
-
- method SiftDown()
- requires MostlyValid;
- requires (forall j :: 4 <= j && j <= n ==> a[j/2] <= a[j]);
- modifies a;
- ensures Valid;
- {
- var i := 1;
- while (2*i <= n) // while i is not a leaf
- invariant 1 <= i && MostlyValid;
- invariant (forall j :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]);
- invariant (forall j :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);
- {
- var smallestChild;
- if (2*i + 1 <= n && a[2*i + 1] < a[2*i]) {
- smallestChild := 2*i + 1;
- } else {
- smallestChild := 2*i;
- }
- if (a[i] <= a[smallestChild]) {
- return;
- }
- a[smallestChild], a[i] := a[i], a[smallestChild];
- i := smallestChild;
- assert 1 <= i/2/2 ==> a[i/2/2] <= a[i];
- }
- }
-}
diff --git a/Test/dafny1/Queue.dfy b/Test/dafny1/Queue.dfy deleted file mode 100644 index 0edfab81..00000000 --- a/Test/dafny1/Queue.dfy +++ /dev/null @@ -1,199 +0,0 @@ -// Queue.dfy
-// Dafny version of Queue.bpl
-// Rustan Leino, 2008
-
-class Queue<T> {
- var head: Node<T>;
- var tail: Node<T>;
-
- ghost var contents: seq<T>;
- ghost var footprint: set<object>;
- ghost var spine: set<Node<T>>;
-
- function Valid(): bool
- reads this, footprint;
- {
- this in footprint && spine <= footprint &&
- head != null && head in spine &&
- tail != null && tail in spine &&
- tail.next == null &&
- (forall n ::
- n in spine ==>
- n != null && n.footprint <= footprint && this !in n.footprint &&
- n.Valid() &&
- (n.next == null ==> n == tail)) &&
- (forall n ::
- n in spine ==>
- n.next != null ==> n.next in spine) &&
- contents == head.tailContents
- }
-
- method Init()
- modifies this;
- ensures Valid() && fresh(footprint - {this});
- ensures |contents| == 0;
- {
- var n := new Node<T>.Init();
- head := n;
- tail := n;
- contents := n.tailContents;
- footprint := {this} + n.footprint;
- spine := {n};
- }
-
- method Rotate()
- requires Valid();
- requires 0 < |contents|;
- modifies footprint;
- ensures Valid() && fresh(footprint - old(footprint));
- ensures contents == old(contents)[1..] + old(contents)[..1];
- {
- var t := Front();
- Dequeue();
- Enqueue(t);
- }
-
- method RotateAny()
- requires Valid();
- requires 0 < |contents|;
- modifies footprint;
- ensures Valid() && fresh(footprint - old(footprint));
- ensures |contents| == |old(contents)|;
- ensures (exists i :: 0 <= i && i <= |contents| &&
- contents == old(contents)[i..] + old(contents)[..i]);
- {
- var t := Front();
- Dequeue();
- Enqueue(t);
- }
-
- method IsEmpty() returns (isEmpty: bool)
- requires Valid();
- ensures isEmpty <==> |contents| == 0;
- {
- isEmpty := head == tail;
- }
-
- method Enqueue(t: T)
- requires Valid();
- modifies footprint;
- ensures Valid() && fresh(footprint - old(footprint));
- ensures contents == old(contents) + [t];
- {
- var n := new Node<T>.Init();
- n.data := t;
- tail.next := n;
- tail := n;
-
- parallel (m | m in spine) {
- m.tailContents := m.tailContents + [t];
- }
- contents := head.tailContents;
-
- parallel (m | m in spine) {
- m.footprint := m.footprint + n.footprint;
- }
- footprint := footprint + n.footprint;
-
- spine := spine + {n};
- }
-
- method Front() returns (t: T)
- requires Valid();
- requires 0 < |contents|;
- ensures t == contents[0];
- {
- t := head.next.data;
- }
-
- method Dequeue()
- requires Valid();
- requires 0 < |contents|;
- modifies footprint;
- ensures Valid() && fresh(footprint - old(footprint));
- ensures contents == old(contents)[1..];
- {
- var n := head.next;
- head := n;
- contents := n.tailContents;
- }
-}
-
-class Node<T> {
- var data: T;
- var next: Node<T>;
-
- ghost var tailContents: seq<T>;
- ghost var footprint: set<object>;
-
- function Valid(): bool
- reads this, footprint;
- {
- this in footprint &&
- (next != null ==> next in footprint && next.footprint <= footprint) &&
- (next == null ==> tailContents == []) &&
- (next != null ==> tailContents == [next.data] + next.tailContents)
- }
-
- method Init()
- modifies this;
- ensures Valid() && fresh(footprint - {this});
- ensures next == null;
- {
- next := null;
- tailContents := [];
- footprint := {this};
- }
-}
-
-class Main<U> {
- method A<T>(t: T, u: T, v: T)
- {
- var q0 := new Queue<T>.Init();
- var q1 := new Queue<T>.Init();
-
- q0.Enqueue(t);
- q0.Enqueue(u);
-
- q1.Enqueue(v);
-
- assert |q0.contents| == 2;
-
- var w := q0.Front();
- assert w == t;
- q0.Dequeue();
-
- w := q0.Front();
- assert w == u;
-
- assert |q0.contents| == 1;
- assert |q1.contents| == 1;
- }
-
- method Main2(t: U, u: U, v: U, q0: Queue<U>, q1: Queue<U>)
- requires q0 != null && q0.Valid();
- requires q1 != null && q1.Valid();
- requires q0.footprint !! q1.footprint;
- requires |q0.contents| == 0;
- modifies q0.footprint, q1.footprint;
- ensures fresh(q0.footprint - old(q0.footprint));
- ensures fresh(q1.footprint - old(q1.footprint));
- {
- q0.Enqueue(t);
- q0.Enqueue(u);
-
- q1.Enqueue(v);
-
- assert |q0.contents| == 2;
-
- var w := q0.Front();
- assert w == t;
- q0.Dequeue();
-
- w := q0.Front();
- assert w == u;
-
- assert |q0.contents| == 1;
- assert |q1.contents| == old(|q1.contents|) + 1;
- }
-}
diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy deleted file mode 100644 index 835c3043..00000000 --- a/Test/dafny1/Rippling.dfy +++ /dev/null @@ -1,617 +0,0 @@ -// Datatypes
-
-datatype Bool = False | True;
-
-datatype Nat = Zero | Suc(Nat);
-
-datatype List = Nil | Cons(Nat, List);
-
-datatype Pair = Pair(Nat, Nat);
-
-datatype PList = PNil | PCons(Pair, PList);
-
-datatype Tree = Leaf | Node(Tree, Nat, Tree);
-
-// Boolean functions
-
-function not(b: Bool): Bool
-{
- match b
- case False => True
- case True => False
-}
-
-function and(a: Bool, b: Bool): Bool
-{
- if a == True && b == True then True else False
-}
-
-// Natural number functions
-
-function add(x: Nat, y: Nat): Nat
-{
- match x
- case Zero => y
- case Suc(w) => Suc(add(w, y))
-}
-
-function minus(x: Nat, y: Nat): Nat
-{
- match x
- case Zero => Zero
- case Suc(a) => match y
- case Zero => x
- case Suc(b) => minus(a, b)
-}
-
-function eq(x: Nat, y: Nat): Bool
-{
- match x
- case Zero => (match y
- case Zero => True
- case Suc(b) => False)
- case Suc(a) => (match y
- case Zero => False
- case Suc(b) => eq(a, b))
-}
-
-function leq(x: Nat, y: Nat): Bool
-{
- match x
- case Zero => True
- case Suc(a) => match y
- case Zero => False
- case Suc(b) => leq(a, b)
-}
-
-function less(x: Nat, y: Nat): Bool
-{
- match y
- case Zero => False
- case Suc(b) => match x
- case Zero => True
- case Suc(a) => less(a, b)
-}
-
-function min(x: Nat, y: Nat): Nat
-{
- match x
- case Zero => Zero
- case Suc(a) => match y
- case Zero => Zero
- case Suc(b) => Suc(min(a, b))
-}
-
-function max(x: Nat, y: Nat): Nat
-{
- match x
- case Zero => y
- case Suc(a) => match y
- case Zero => x
- case Suc(b) => Suc(max(a, b))
-}
-
-// List functions
-
-function concat(xs: List, ys: List): List
-{
- match xs
- case Nil => ys
- case Cons(x,tail) => Cons(x, concat(tail, ys))
-}
-
-function mem(x: Nat, xs: List): Bool
-{
- match xs
- case Nil => False
- case Cons(y, ys) => if x == y then True else mem(x, ys)
-}
-
-function delete(n: Nat, xs: List): List
-{
- match xs
- case Nil => Nil
- case Cons(y, ys) =>
- if y == n then delete(n, ys) else Cons(y, delete(n, ys))
-}
-
-function drop(n: Nat, xs: List): List
-{
- match n
- case Zero => xs
- case Suc(m) => match xs
- case Nil => Nil
- case Cons(x, tail) => drop(m, tail)
-}
-
-function take(n: Nat, xs: List): List
-{
- match n
- case Zero => Nil
- case Suc(m) => match xs
- case Nil => Nil
- case Cons(x, tail) => Cons(x, take(m, tail))
-}
-
-function len(xs: List): Nat
-{
- match xs
- case Nil => Zero
- case Cons(y, ys) => Suc(len(ys))
-}
-
-function count(x: Nat, xs: List): Nat
-{
- match xs
- case Nil => Zero
- case Cons(y, ys) =>
- if x == y then Suc(count(x, ys)) else count(x, ys)
-}
-
-function last(xs: List): Nat
-{
- match xs
- case Nil => Zero
- case Cons(y, ys) => match ys
- case Nil => y
- case Cons(z, zs) => last(ys)
-}
-
-function apply(f: FunctionValue, xs: List): List
-{
- match xs
- case Nil => Nil
- case Cons(y, ys) => Cons(Apply(f, y), apply(f, ys))
-}
-
-// In the following two functions, parameter "p" stands for a predicate: applying p and
-// getting Zero means "false" and getting anything else means "true".
-
-function takeWhileAlways(p: FunctionValue, xs: List): List
-{
- match xs
- case Nil => Nil
- case Cons(y, ys) =>
- if Apply(p, y) != Zero
- then Cons(y, takeWhileAlways(p, ys))
- else Nil
-}
-
-function dropWhileAlways(p: FunctionValue, xs: List): List
-{
- match xs
- case Nil => Nil
- case Cons(y, ys) =>
- if Apply(p, y) != Zero
- then dropWhileAlways(p, ys)
- else Cons(y, ys)
-}
-
-function filter(p: FunctionValue, xs: List): List
-{
- match xs
- case Nil => Nil
- case Cons(y, ys) =>
- if Apply(p, y) != Zero
- then Cons(y, filter(p, ys))
- else filter(p, ys)
-}
-
-function insort(n: Nat, xs: List): List
-{
- match xs
- case Nil => Cons(n, Nil)
- case Cons(y, ys) =>
- if leq(n, y) == True
- then Cons(n, Cons(y, ys))
- else Cons(y, ins(n, ys))
-}
-
-function ins(n: Nat, xs: List): List
-{
- match xs
- case Nil => Cons(n, Nil)
- case Cons(y, ys) =>
- if less(n, y) == True
- then Cons(n, Cons(y, ys))
- else Cons(y, ins(n, ys))
-}
-
-function ins1(n: Nat, xs: List): List
-{
- match xs
- case Nil => Cons(n, Nil)
- case Cons(y, ys) =>
- if n == y
- then Cons(y, ys)
- else Cons(y, ins1(n, ys))
-}
-
-function sort(xs: List): List
-{
- match xs
- case Nil => Nil
- case Cons(y, ys) => insort(y, sort(ys))
-}
-
-function reverse(xs: List): List
-{
- match xs
- case Nil => Nil
- case Cons(t, rest) => concat(reverse(rest), Cons(t, Nil))
-}
-
-// Pair list functions
-
-function zip(a: List, b: List): PList
-{
- match a
- case Nil => PNil
- case Cons(x, xs) => match b
- case Nil => PNil
- case Cons(y, ys) => PCons(Pair.Pair(x, y), zip(xs, ys))
-}
-
-function zipConcat(x: Nat, xs: List, more: List): PList
-{
- match more
- case Nil => PNil
- case Cons(y, ys) => PCons(Pair.Pair(x, y), zip(xs, ys))
-}
-
-// Binary tree functions
-
-function height(t: Tree): Nat
-{
- match t
- case Leaf => Zero
- case Node(l, x, r) => Suc(max(height(l), height(r)))
-}
-
-function mirror(t: Tree): Tree
-{
- match t
- case Leaf => Leaf
- case Node(l, x, r) => Node(mirror(r), x, mirror(l))
-}
-
-// Function parameters
-
-// Dafny currently does not support passing functions as arguments. To simulate
-// arbitrary functions, the following type and Apply function play the role of
-// applying some prescribed function (here, a value of the type)
-// to some argument.
-
-type FunctionValue;
-function Apply(f: FunctionValue, x: Nat): Nat // this function is left uninterpreted
-
-// The following functions stand for the constant "false" and "true" functions,
-// respectively.
-
-function AlwaysFalseFunction(): FunctionValue
- ensures forall n :: Apply(AlwaysFalseFunction(), n) == Zero;
-function AlwaysTrueFunction(): FunctionValue
- ensures forall n :: Apply(AlwaysTrueFunction(), n) != Zero;
-
-// -----------------------------------------------------------------------------------
-// The theorems to be proved
-// -----------------------------------------------------------------------------------
-
-ghost method P1()
- ensures forall n, xs :: concat(take(n, xs), drop(n, xs)) == xs;
-{
-}
-
-ghost method P2()
- ensures forall n, xs, ys :: add(count(n, xs), count(n, ys)) == count(n, concat(xs, ys));
-{
-}
-
-ghost method P3()
- ensures forall n, xs, ys :: leq(count(n, xs), count(n, concat(xs, ys))) == True;
-{
-}
-
-ghost method P4()
- ensures forall n, xs :: add(Suc(Zero), count(n, xs)) == count(n, Cons(n, xs));
-{
-}
-
-ghost method P5()
- ensures forall n, xs, x ::
- add(Suc(Zero), count(n, xs)) == count(n, Cons(x, xs))
- ==> n == x;
-{
-}
-
-ghost method P6()
- ensures forall m, n :: minus(n, add(n, m)) == Zero;
-{
-}
-
-ghost method P7()
- ensures forall m, n :: minus(add(n, m), n) == m;
-{
-}
-
-ghost method P8()
- ensures forall k, m, n :: minus(add(k, m), add(k, n)) == minus(m, n);
-{
-}
-
-ghost method P9()
- ensures forall i, j, k :: minus(minus(i, j), k) == minus(i, add(j, k));
-{
-}
-
-ghost method P10()
- ensures forall m :: minus(m, m) == Zero;
-{
-}
-
-ghost method P11()
- ensures forall xs :: drop(Zero, xs) == xs;
-{
-}
-
-ghost method P12()
- ensures forall n, xs, f :: drop(n, apply(f, xs)) == apply(f, drop(n, xs));
-{
-}
-
-ghost method P13()
- ensures forall n, x, xs :: drop(Suc(n), Cons(x, xs)) == drop(n, xs);
-{
-}
-
-ghost method P14()
- ensures forall xs, ys, p :: filter(p, concat(xs, ys)) == concat(filter(p, xs), filter(p, ys));
-{
-}
-
-ghost method P15()
- ensures forall x, xs :: len(ins(x, xs)) == Suc(len(xs));
-{
-}
-
-ghost method P16()
- ensures forall x, xs :: xs == Nil ==> last(Cons(x, xs)) == x;
-{
-}
-
-ghost method P17()
- ensures forall n :: leq(n, Zero) == True <==> n == Zero;
-{
-}
-
-ghost method P18()
- ensures forall i, m :: less(i, Suc(add(i, m))) == True;
-{
-}
-
-ghost method P19()
- ensures forall n, xs :: len(drop(n, xs)) == minus(len(xs), n);
-{
-}
-
-ghost method P20()
- ensures forall xs :: len(sort(xs)) == len(xs);
-{
- P15(); // use the statement of problem 15 as a lemma
- // ... and manually introduce a case distinction:
- assert forall ys ::
- sort(ys) == Nil ||
- exists z, zs :: sort(ys) == Cons(z, zs);
-}
-
-ghost method P21()
- ensures forall n, m :: leq(n, add(n, m)) == True;
-{
-}
-
-ghost method P22()
- ensures forall a, b, c :: max(max(a, b), c) == max(a, max(b, c));
-{
-}
-
-ghost method P23()
- ensures forall a, b :: max(a, b) == max(b, a);
-{
-}
-
-ghost method P24()
- ensures forall a, b :: max(a, b) == a <==> leq(b, a) == True;
-{
-}
-
-ghost method P25()
- ensures forall a, b :: max(a, b) == b <==> leq(a, b) == True;
-{
-}
-
-ghost method P26()
- ensures forall x, xs, ys :: mem(x, xs) == True ==> mem(x, concat(xs, ys)) == True;
-{
-}
-
-ghost method P27()
- ensures forall x, xs, ys :: mem(x, ys) == True ==> mem(x, concat(xs, ys)) == True;
-{
-}
-
-ghost method P28()
- ensures forall x, xs :: mem(x, concat(xs, Cons(x, Nil))) == True;
-{
-}
-
-ghost method P29()
- ensures forall x, xs :: mem(x, ins1(x, xs)) == True;
-{
-}
-
-ghost method P30()
- ensures forall x, xs :: mem(x, ins(x, xs)) == True;
-{
-}
-
-ghost method P31()
- ensures forall a, b, c :: min(min(a, b), c) == min(a, min(b, c));
-{
-}
-
-ghost method P32()
- ensures forall a, b :: min(a, b) == min(b, a);
-{
-}
-
-ghost method P33()
- ensures forall a, b :: min(a, b) == a <==> leq(a, b) == True;
-{
-}
-
-ghost method P34()
- ensures forall a, b :: min(a, b) == b <==> leq(b, a) == True;
-{
-}
-
-ghost method P35()
- ensures forall xs :: dropWhileAlways(AlwaysFalseFunction(), xs) == xs;
-{
-}
-
-ghost method P36()
- ensures forall xs :: takeWhileAlways(AlwaysTrueFunction(), xs) == xs;
-{
-}
-
-ghost method P37()
- ensures forall x, xs :: not(mem(x, delete(x, xs))) == True;
-{
-}
-
-ghost method P38()
- ensures forall n, xs :: count(n, concat(xs, Cons(n, Nil))) == Suc(count(n, xs));
-{
-}
-
-ghost method P39()
- ensures forall n, x, xs ::
- add(count(n, Cons(x, Nil)), count(n, xs)) == count(n, Cons(x, xs));
-{
-}
-
-ghost method P40()
- ensures forall xs :: take(Zero, xs) == Nil;
-{
-}
-
-ghost method P41()
- ensures forall n, xs, f :: take(n, apply(f, xs)) == apply(f, take(n, xs));
-{
-}
-
-ghost method P42()
- ensures forall n, x, xs :: take(Suc(n), Cons(x, xs)) == Cons(x, take(n, xs));
-{
-}
-
-ghost method P43(p: FunctionValue)
- ensures forall xs :: concat(takeWhileAlways(p, xs), dropWhileAlways(p, xs)) == xs;
-{
-}
-
-ghost method P44()
- ensures forall x, xs, ys :: zip(Cons(x, xs), ys) == zipConcat(x, xs, ys);
-{
-}
-
-ghost method P45()
- ensures forall x, xs, y, ys ::
- zip(Cons(x, xs), Cons(y, ys)) ==
- PCons(Pair.Pair(x, y), zip(xs, ys));
-{
-}
-
-ghost method P46()
- ensures forall ys :: zip(Nil, ys) == PNil;
-{
-}
-
-ghost method P47()
- ensures forall a :: height(mirror(a)) == height(a);
-{
- // proving this theorem requires a previously proved lemma:
- P23();
-}
-
-// ...
-
-ghost method P54()
- ensures forall m, n :: minus(add(m, n), n) == m;
-{
- // the proof of this theorem follows from two lemmas:
- assert forall m, n :: minus(add(n, m), n) == m;
- assert forall m, n :: add(m, n) == add(n, m);
-}
-
-ghost method P65()
- ensures forall i, m :: less(i, Suc(add(m, i))) == True;
-{
- if (*) {
- // the proof of this theorem follows from two lemmas:
- assert forall i, m :: less(i, Suc(add(i, m))) == True;
- assert forall m, n :: add(m, n) == add(n, m);
- } else {
- // a different way to prove it uses the following lemma:
- assert forall x,y :: add(x, Suc(y)) == Suc(add(x,y));
- }
-}
-
-ghost method P67()
- ensures forall m, n :: leq(n, add(m, n)) == True;
-{
- if (*) {
- // the proof of this theorem follows from two lemmas:
- assert forall m, n :: leq(n, add(n, m)) == True;
- assert forall m, n :: add(m, n) == add(n, m);
- } else {
- // a different way to prove it uses the following lemma:
- assert forall x,y :: add(x, Suc(y)) == Suc(add(x,y));
- }
-}
-
-// ---------
-// Here is a alternate way of writing down the proof obligations:
-
-ghost method P1_alt(n: Nat, xs: List)
- ensures concat(take(n, xs), drop(n, xs)) == xs;
-{
-}
-
-ghost method P2_alt(n: Nat, xs: List, ys: List)
- ensures add(count(n, xs), count(n, ys)) == count(n, (concat(xs, ys)));
-{
-}
-
-// ---------
-
-ghost method Lemma_RevConcat(xs: List, ys: List)
- ensures reverse(concat(xs, ys)) == concat(reverse(ys), reverse(xs));
-{
- match (xs) {
- case Nil =>
- assert forall ws :: concat(ws, Nil) == ws;
- case Cons(t, rest) =>
- assert forall a, b, c :: concat(a, concat(b, c)) == concat(concat(a, b), c);
- }
-}
-
-ghost method Theorem(xs: List)
- ensures reverse(reverse(xs)) == xs;
-{
- match (xs) {
- case Nil =>
- case Cons(t, rest) =>
- Lemma_RevConcat(reverse(rest), Cons(t, Nil));
- }
-}
diff --git a/Test/dafny1/SchorrWaite-stages.dfy b/Test/dafny1/SchorrWaite-stages.dfy deleted file mode 100644 index 094e7be7..00000000 --- a/Test/dafny1/SchorrWaite-stages.dfy +++ /dev/null @@ -1,267 +0,0 @@ -// Schorr-Waite algorithms, written and verified in Dafny.
-// Rustan Leino
-// Original version: 7 November 2008
-// Version with proof divided into stages: June 2012.
-// Copyright (c) 2008-2012 Microsoft.
-
-ghost module M0 {
- // In this module, we declare the Node class, the definition of Reachability, and the specification
- // and implementation of the Schorr-Waite algorithm.
-
- class Node {
- var children: seq<Node>;
- var marked: bool;
- var childrenVisited: nat;
- }
-
- datatype Path = Empty | Extend(Path, Node);
-
- function Reachable(source: Node, sink: Node, S: set<Node>): bool
- requires null !in S;
- reads S;
- {
- exists via: Path :: ReachableVia(source, via, sink, S)
- }
-
- function ReachableVia(source: Node, p: Path, sink: Node, S: set<Node>): bool
- requires null !in S;
- reads S;
- decreases p;
- {
- match p
- case Empty => source == sink
- case Extend(prefix, n) => n in S && sink in n.children && ReachableVia(source, prefix, n, S)
- }
-
- method SchorrWaite(root: Node, ghost S: set<Node>)
- requires root in S;
- // S is closed under 'children':
- requires forall n :: n in S ==> n != null &&
- forall ch :: ch in n.children ==> ch == null || ch in S;
- // the graph starts off with nothing marked and nothing being indicated as currently being visited:
- requires forall n :: n in S ==> !n.marked && n.childrenVisited == 0;
- modifies S;
- // nodes reachable from 'root' are marked:
- ensures root.marked;
- ensures forall n :: n in S && n.marked ==>
- forall ch :: ch in n.children && ch != null ==> ch.marked;
- // every marked node was reachable from 'root' in the pre-state:
- ensures forall n :: n in S && n.marked ==> old(Reachable(root, n, S));
- // the structure of the graph has not changed:
- ensures forall n :: n in S ==>
- n.childrenVisited == old(n.childrenVisited) &&
- n.children == old(n.children);
- {
- root.marked := true;
- var t, p := root, null;
- ghost var stackNodes := [];
- while (true)
- // stackNodes is a sequence of nodes from S:
- invariant forall n :: n in stackNodes ==> n in S;
-
- // The current node, t, is not included in stackNodes. Rather, t is just above the top of stackNodes.
- // We say that the stack stackNodes+[t] are the "active" nodes.
- invariant t in S && t !in stackNodes;
-
- // p points to the parent of the current node, that is, the node through which t was encountered in the
- // depth-first traversal. This amounts to being the top of stackNodes, or null if stackNodes is empty.
- // Note, it may seem like the variable p is redundant, since it holds a value that can be computed
- // from stackNodes. But note that stackNodes is a ghost variable and won't be present at run
- // time, where p is a physical variable that will be present at run time.
- invariant p == if |stackNodes| == 0 then null else stackNodes[|stackNodes|-1];
-
- // The .childrenVisited field is the extra information that the Schorr-Waite algorithm needs. It
- // is used only for the active nodes, where it keeps track of how many of a node's children have been
- // processed. For the nodes on stackNodes, .childrenVisited is less than the number of children, so
- // it is an index of a child. For t, .childrenVisited may be as large as all of the children, which
- // indicates that the node is ready to be popped off the stack of active nodes. For all other nodes,
- // .childrenVisited is the original value, which is 0.
- invariant forall n :: n in stackNodes ==> n.childrenVisited < |n.children|;
- invariant t.childrenVisited <= |t.children|;
- invariant forall n :: n in S && n !in stackNodes && n != t ==> n.childrenVisited == 0;
-
- // To represent the stackNodes, the algorithm reverses children pointers. It never changes the number
- // of children a node has. The only nodes with children pointers different than the original values are
- // the nodes on stackNodes; moreover, only the index of the currently active child of a node is different.
- invariant forall n :: n in stackNodes ==>
- |n.children| == old(|n.children|) &&
- forall j :: 0 <= j < |n.children| ==> j == n.childrenVisited || n.children[j] == old(n.children[j]);
- invariant forall n :: n in S && n !in stackNodes ==> n.children == old(n.children);
-
- // The children pointers that have been changed form a stack. That is, the active child of stackNodes[k]
- // points to stackNodes[k-1], with the end case pointing to null.
- invariant 0 < |stackNodes| ==>
- stackNodes[0].children[stackNodes[0].childrenVisited] == null;
- invariant forall k :: 0 < k < |stackNodes| ==>
- stackNodes[k].children[stackNodes[k].childrenVisited] == stackNodes[k-1];
- // We also need to keep track of what the original values of the children pointers had been. Here, we
- // have that the active child of stackNodes[k] used to be stackNodes[k+1], with the end case pointing
- // to t.
- invariant forall k :: 0 <= k < |stackNodes|-1 ==>
- old(stackNodes[k].children)[stackNodes[k].childrenVisited] == stackNodes[k+1];
- invariant 0 < |stackNodes| ==>
- old(stackNodes[|stackNodes|-1].children)[stackNodes[|stackNodes|-1].childrenVisited] == t;
-
- decreases *; // leave termination checking for a later refinement
- {
- if (t.childrenVisited == |t.children|) {
- // pop
- t.childrenVisited := 0;
- if (p == null) { break; }
-
- t, p, p.children := p, p.children[p.childrenVisited], p.children[p.childrenVisited := t];
- stackNodes := stackNodes[..|stackNodes| - 1];
- t.childrenVisited := t.childrenVisited + 1;
-
- } else if (t.children[t.childrenVisited] == null || t.children[t.childrenVisited].marked) {
- // just advance to next child
- t.childrenVisited := t.childrenVisited + 1;
-
- } else {
- // push
- stackNodes := stackNodes + [t];
- t, p, t.children := t.children[t.childrenVisited], t, t.children[t.childrenVisited := p];
- t.marked := true;
-
- // To prove that this "if" branch maintains the invariant "t !in stackNodes" will require
- // some more properties about the loop. Therefore, we just assume the property here and
- // prove it in a separate refinement.
- assume t !in stackNodes;
- }
- }
- // From the loop invariant, it now follows that all children pointers have been restored,
- // and so have all .childrenVisited fields. Thus, the last postcondition (the one that says
- // the structure of the graph has not been changed) has been established.
- // Eventually, we also need to prove that exactly the right nodes have been marked,
- // but let's just assume those properties for now and prove them in later refinements:
- assume root.marked && forall n :: n in S && n.marked ==>
- forall ch :: ch in n.children && ch != null ==> ch.marked;
- assume forall n :: n in S && n.marked ==> old(Reachable(root, n, S));
- }
-}
-
-ghost module M1 refines M0 {
- // In this superposition, we start reasoning about the marks. In particular, we prove that the method
- // marks all reachable nodes.
- method SchorrWaite...
- {
- ...;
- while ...
- // The loop keeps marking nodes: The root is always marked. All children of any marked non-active
- // node are marked. Active nodes are marked, and the first .childrenVisited of every active node
- // are marked.
- invariant root.marked;
- invariant forall n :: n in S && n.marked && n !in stackNodes && n != t ==>
- forall ch :: ch in n.children && ch != null ==> ch.marked;
- invariant forall n :: n in stackNodes || n == t ==>
- n.marked &&
- forall j :: 0 <= j < n.childrenVisited ==> n.children[j] == null || n.children[j].marked;
-
- decreases *; // keep postponing termination checking
- {
- if ... { // pop
- } else if ... { // next child
- } else { // push
- ...;
- // With the new loop invariants, we know that all active nodes are marked. Since the new value
- // of "t" was not marked at the beginning of this iteration, we can now prove that the invariant
- // "t !in stackNodes" is maintained, so we'll refine the assume from above with an assert.
- assert ...;
- }
- }
- // The new loop invariants give us a lower bound on which nodes are marked. Hence, we can now
- // discharge the "everything reachable is marked" postcondition, whose proof we postponed above
- // by supplying an assume statement. Here, we refine that assume statement into an assert.
- assert ...;
- }
-}
-
-ghost module M2 refines M1 {
- // In this superposition, we prove that only reachable nodes are marked. Essentially, we want
- // to add a loop invariant that says t is reachable from root, because then the loop invariant
- // that marked nodes are reachable follows. More precisely, we need to say that the node
- // referenced by t is *in the initial state* reachable from root--because as we change
- // children pointers during the course of the algorithm, what is reachable at some point in
- // time may be different from what was reachable initially.
-
- // To do our proof, which involves establishing reachability between various nodes, we need
- // some additional bookkeeping. In particular, we keep track of the path from root to t,
- // and we associate with every marked node the path to it from root. The former is easily
- // maintained in a local ghost variable; the latter is most easily represented as a ghost
- // field in each node (an alternative would be to have a local variable that is a map from
- // nodes to paths). So, we add a field declaration to the Node class:
- class Node {
- ghost var pathFromRoot: Path;
- }
-
- method SchorrWaite...
- {
- ghost var path := Path.Empty;
- root.pathFromRoot := path;
- ...;
- while ...
- // There's a subtle complication when we speak of old(ReachableVia(... P ...)) for a path
- // P. The expression old(...) says to evaluate the expression "..." in the pre-state of
- // the method. So, old(ReachableVia(...)) says to evaluate ReachableVia(...) in the pre-
- // state of the method. But in order for the "old(...)" expression to be well-formed,
- // the subexpressions of the "..." must only refer to values that existed in the pre-state
- // of the method. This incurs the proof obligation that any objects referenced by the
- // parameters of ReachableVia(...) must have been allocated in the pre-state of the
- // method. The proof obligation is easy to establish for root, t, and S (since root and
- // S were given as in-parameters to the method, and we have "t in S"). But what about
- // the path argument to ReachableVia? Since datatype values of type Path contain object
- // references, we need to make sure we can deal with the proof obligation for the path
- // argument. For this reason, we add invariants that say that "path" and the .pathFromRoot
- // field of all marked nodes contain values that make sense in the pre-state.
- invariant !fresh(path) && old(ReachableVia(root, path, t, S));
- invariant forall n :: n in S && n.marked ==> var pth := n.pathFromRoot;
- !fresh(pth) && old(ReachableVia(root, pth, n, S));
- invariant forall n :: n in S && n.marked ==> old(Reachable(root, n, S));
-
- decreases *; // keep postponing termination checking
- {
- if ... {
- // pop
- ...;
- path := t.pathFromRoot;
- } else if ... {
- // advance to next child
- } else {
- // push
- path := Path.Extend(path, t);
- ...;
- t.pathFromRoot := path;
- }
- }
- // In M0 above, we placed two assume statements here. In M1, we refined the first of these
- // into an assert. We repeat that assert here:
- assert ...;
- // And now we we refine the second assume into an assert, proving that only reachable nodes
- // have been marked.
- assert ...;
- }
-}
-
-module M3 refines M2 {
- // In this final superposition, we prove termination of the loop.
- method SchorrWaite...
- {
- // The loop variant is a lexicographic triple, consisting of (0) the set of unmarked
- // nodes, (1) the (length of the) stackNodes sequence, and (2) the number children of
- // the current node that are still to be investigated. We introduce a ghost variable
- // to keep track of the set of unmarked nodes.
- ghost var unmarkedNodes := S - {root};
- ...;
- while ...
- invariant forall n :: n in S && !n.marked ==> n in unmarkedNodes;
- decreases unmarkedNodes, stackNodes, |t.children| - t.childrenVisited;
- {
- if ... { // pop
- } else if ... { // next child
- } else { // push
- ...;
- unmarkedNodes := unmarkedNodes - {t};
- }
- }
- }
-}
diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy deleted file mode 100644 index 18adf491..00000000 --- a/Test/dafny1/SchorrWaite.dfy +++ /dev/null @@ -1,270 +0,0 @@ -// Rustan Leino
-// 7 November 2008
-// Schorr-Waite and other marking algorithms, written and verified in Dafny.
-// Copyright (c) 2008, Microsoft.
-
-class Node {
- var children: seq<Node>;
- var marked: bool;
- var childrenVisited: int;
- ghost var pathFromRoot: Path;
-}
-
-datatype Path = Empty | Extend(Path, Node);
-
-
-class Main {
- method RecursiveMark(root: Node, ghost S: set<Node>)
- requires root in S;
- // S is closed under 'children':
- requires (forall n :: n in S ==> n != null &&
- (forall ch :: ch in n.children ==> ch == null || ch in S));
- requires (forall n :: n in S ==> ! n.marked && n.childrenVisited == 0);
- modifies S;
- ensures root.marked;
- // nodes reachable from 'root' are marked:
- ensures (forall n :: n in S && n.marked ==>
- (forall ch :: ch in n.children && ch != null ==> ch.marked));
- ensures (forall n :: n in S ==>
- n.childrenVisited == old(n.childrenVisited) &&
- n.children == old(n.children));
- {
- RecursiveMarkWorker(root, S, {});
- }
-
- method RecursiveMarkWorker(root: Node, ghost S: set<Node>, ghost stackNodes: set<Node>)
- requires root != null && root in S;
- requires (forall n :: n in S ==> n != null &&
- (forall ch :: ch in n.children ==> ch == null || ch in S));
- requires (forall n :: n in S && n.marked ==>
- n in stackNodes ||
- (forall ch :: ch in n.children && ch != null ==> ch.marked));
- requires (forall n :: n in stackNodes ==> n != null && n.marked);
- modifies S;
- ensures root.marked;
- // nodes reachable from 'root' are marked:
- ensures (forall n :: n in S && n.marked ==>
- n in stackNodes ||
- (forall ch :: ch in n.children && ch != null ==> ch.marked));
- ensures (forall n: Node :: n in S && old(n.marked) ==> n.marked);
- ensures (forall n :: n in S ==>
- n.childrenVisited == old(n.childrenVisited) &&
- n.children == old(n.children));
- decreases S - stackNodes;
- {
- if (! root.marked) {
- root.marked := true;
- var i := 0;
- while (i < |root.children|)
- invariant root.marked && i <= |root.children|;
- invariant (forall n :: n in S && n.marked ==>
- n == root ||
- n in stackNodes ||
- (forall ch :: ch in n.children && ch != null ==> ch.marked));
- invariant (forall j :: 0 <= j && j < i ==>
- root.children[j] == null || root.children[j].marked);
- invariant (forall n: Node :: n in S && old(n.marked) ==> n.marked);
- invariant (forall n :: n in S ==>
- n.childrenVisited == old(n.childrenVisited) &&
- n.children == old(n.children));
- {
- var c := root.children[i];
- if (c != null) {
- RecursiveMarkWorker(c, S, stackNodes + {root});
- }
- i := i + 1;
- }
- }
- }
-
- // ---------------------------------------------------------------------------------
-
- method IterativeMark(root: Node, ghost S: set<Node>)
- requires root in S;
- // S is closed under 'children':
- requires (forall n :: n in S ==> n != null &&
- (forall ch :: ch in n.children ==> ch == null || ch in S));
- requires (forall n :: n in S ==> ! n.marked && n.childrenVisited == 0);
- modifies S;
- ensures root.marked;
- // nodes reachable from 'root' are marked:
- ensures (forall n :: n in S && n.marked ==>
- (forall ch :: ch in n.children && ch != null ==> ch.marked));
- ensures (forall n :: n in S ==>
- n.childrenVisited == old(n.childrenVisited) &&
- n.children == old(n.children));
- {
- var t := root;
- t.marked := true;
- var stackNodes := [];
- ghost var unmarkedNodes := S - {t};
- while (true)
- invariant root.marked && t in S && t !in stackNodes;
- // stackNodes has no duplicates:
- invariant (forall i, j :: 0 <= i && i < j && j < |stackNodes| ==>
- stackNodes[i] != stackNodes[j]);
- invariant (forall n :: n in stackNodes ==> n in S);
- invariant (forall n :: n in stackNodes || n == t ==>
- n.marked &&
- 0 <= n.childrenVisited && n.childrenVisited <= |n.children| &&
- (forall j :: 0 <= j && j < n.childrenVisited ==>
- n.children[j] == null || n.children[j].marked));
- invariant (forall n :: n in stackNodes ==> n.childrenVisited < |n.children|);
- // nodes on the stack are linked:
- invariant (forall j :: 0 <= j && j+1 < |stackNodes| ==>
- stackNodes[j].children[stackNodes[j].childrenVisited] == stackNodes[j+1]);
- invariant 0 < |stackNodes| ==>
- stackNodes[|stackNodes|-1].children[stackNodes[|stackNodes|-1].childrenVisited] == t;
- invariant (forall n :: n in S && n.marked && n !in stackNodes && n != t ==>
- (forall ch :: ch in n.children && ch != null ==> ch.marked));
- invariant (forall n :: n in S && n !in stackNodes && n != t ==>
- n.childrenVisited == old(n.childrenVisited));
- invariant (forall n: Node :: n in S ==> n.children == old(n.children));
- invariant (forall n :: n in S && !n.marked ==> n in unmarkedNodes);
- decreases unmarkedNodes, stackNodes, |t.children| - t.childrenVisited;
- {
- if (t.childrenVisited == |t.children|) {
- // pop
- t.childrenVisited := 0;
- if (|stackNodes| == 0) {
- return;
- }
- t := stackNodes[|stackNodes| - 1];
- stackNodes := stackNodes[..|stackNodes| - 1];
- t.childrenVisited := t.childrenVisited + 1;
- } else if (t.children[t.childrenVisited] == null || t.children[t.childrenVisited].marked) {
- // just advance to next child
- t.childrenVisited := t.childrenVisited + 1;
- } else {
- // push
- stackNodes := stackNodes + [t];
- t := t.children[t.childrenVisited];
- t.marked := true;
- unmarkedNodes := unmarkedNodes - {t};
- }
- }
- }
-
- // ---------------------------------------------------------------------------------
-
- function Reachable(from: Node, to: Node, S: set<Node>): bool
- requires null !in S;
- reads S;
- {
- (exists via: Path :: ReachableVia(from, via, to, S))
- }
-
- function ReachableVia(from: Node, via: Path, to: Node, S: set<Node>): bool
- requires null !in S;
- reads S;
- decreases via;
- {
- match via
- case Empty => from == to
- case Extend(prefix, n) => n in S && to in n.children && ReachableVia(from, prefix, n, S)
- }
-
- method SchorrWaite(root: Node, ghost S: set<Node>)
- requires root in S;
- // S is closed under 'children':
- requires (forall n :: n in S ==> n != null &&
- (forall ch :: ch in n.children ==> ch == null || ch in S));
- // the graph starts off with nothing marked and nothing being indicated as currently being visited:
- requires (forall n :: n in S ==> ! n.marked && n.childrenVisited == 0);
- modifies S;
- // nodes reachable from 'root' are marked:
- ensures root.marked;
- ensures (forall n :: n in S && n.marked ==>
- (forall ch :: ch in n.children && ch != null ==> ch.marked));
- // every marked node was reachable from 'root' in the pre-state:
- ensures (forall n :: n in S && n.marked ==> old(Reachable(root, n, S)));
- // the structure of the graph has not changed:
- ensures (forall n :: n in S ==>
- n.childrenVisited == old(n.childrenVisited) &&
- n.children == old(n.children));
- {
- var t := root;
- var p: Node := null; // parent of t in original graph
- ghost var path := Path.Empty;
- t.marked := true;
- t.pathFromRoot := path;
- ghost var stackNodes := [];
- ghost var unmarkedNodes := S - {t};
- while (true)
- invariant root.marked && t != null && t in S && t !in stackNodes;
- invariant |stackNodes| == 0 <==> p == null;
- invariant 0 < |stackNodes| ==> p == stackNodes[|stackNodes|-1];
- // stackNodes has no duplicates:
- invariant (forall i, j :: 0 <= i && i < j && j < |stackNodes| ==>
- stackNodes[i] != stackNodes[j]);
- invariant (forall n :: n in stackNodes ==> n in S);
- invariant (forall n :: n in stackNodes || n == t ==>
- n.marked &&
- 0 <= n.childrenVisited && n.childrenVisited <= |n.children| &&
- (forall j :: 0 <= j && j < n.childrenVisited ==>
- n.children[j] == null || n.children[j].marked));
- invariant (forall n :: n in stackNodes ==> n.childrenVisited < |n.children|);
- invariant (forall n :: n in S && n.marked && n !in stackNodes && n != t ==>
- (forall ch :: ch in n.children && ch != null ==> ch.marked));
- invariant (forall n :: n in S && n !in stackNodes && n != t ==>
- n.childrenVisited == old(n.childrenVisited));
- invariant (forall n :: n in S ==> n in stackNodes || n.children == old(n.children));
- invariant (forall n :: n in stackNodes ==>
- |n.children| == old(|n.children|) &&
- (forall j :: 0 <= j && j < |n.children| ==>
- j == n.childrenVisited || n.children[j] == old(n.children[j])));
- // every marked node is reachable:
- invariant !fresh(path); // needed to show 'path' worthy as argument to old(Reachable(...))
- invariant old(ReachableVia(root, path, t, S));
- invariant (forall n, pth :: n in S && n.marked && pth == n.pathFromRoot ==> !fresh(pth));
- invariant (forall n, pth :: n in S && n.marked && pth == n.pathFromRoot ==>
- old(ReachableVia(root, pth, n, S)));
- invariant (forall n :: n in S && n.marked ==> old(Reachable(root, n, S)));
- // the current values of m.children[m.childrenVisited] for m's on the stack:
- invariant 0 < |stackNodes| ==> stackNodes[0].children[stackNodes[0].childrenVisited] == null;
- invariant (forall k :: 0 < k && k < |stackNodes| ==>
- stackNodes[k].children[stackNodes[k].childrenVisited] == stackNodes[k-1]);
- // the original values of m.children[m.childrenVisited] for m's on the stack:
- invariant (forall k :: 0 <= k && k+1 < |stackNodes| ==>
- old(stackNodes[k].children)[stackNodes[k].childrenVisited] == stackNodes[k+1]);
- invariant 0 < |stackNodes| ==>
- old(stackNodes[|stackNodes|-1].children)[stackNodes[|stackNodes|-1].childrenVisited] == t;
- invariant (forall n :: n in S && !n.marked ==> n in unmarkedNodes);
- decreases unmarkedNodes, stackNodes, |t.children| - t.childrenVisited;
- {
- if (t.childrenVisited == |t.children|) {
- // pop
- t.childrenVisited := 0;
- if (p == null) {
- return;
- }
- var oldP := p.children[p.childrenVisited];
- // p.children[p.childrenVisited] := t;
- p.children := p.children[..p.childrenVisited] + [t] + p.children[p.childrenVisited + 1..];
- t := p;
- p := oldP;
- stackNodes := stackNodes[..|stackNodes| - 1];
- t.childrenVisited := t.childrenVisited + 1;
- path := t.pathFromRoot;
-
- } else if (t.children[t.childrenVisited] == null || t.children[t.childrenVisited].marked) {
- // just advance to next child
- t.childrenVisited := t.childrenVisited + 1;
-
- } else {
- // push
-
- var newT := t.children[t.childrenVisited];
- // t.children[t.childrenVisited] := p;
- t.children := t.children[..t.childrenVisited] + [p] + t.children[t.childrenVisited + 1..];
- p := t;
- stackNodes := stackNodes + [t];
- path := Path.Extend(path, t);
- t := newT;
- t.marked := true;
- t.pathFromRoot := path;
- unmarkedNodes := unmarkedNodes - {t};
- }
- }
- }
-}
diff --git a/Test/dafny1/SeparationLogicList.dfy b/Test/dafny1/SeparationLogicList.dfy deleted file mode 100644 index 56a64bd6..00000000 --- a/Test/dafny1/SeparationLogicList.dfy +++ /dev/null @@ -1,169 +0,0 @@ -// This file contains three variations of the separation-logic lseg linked-list example.
-
-// In this first variation, the auxiliary information about the contents represented by a linked list
-// and the subpart of the heap that the list occupies is passed around as additional parameters. In
-// separation logic, the contents (here called 'q') would indeed be passed around in that way, whereas
-// separating conjunction and the abstract predicate ListSegment would take care of staking out which
-// subpart of the heap is being occupied by the linked-list representation.
-class Node<T> {
- var data: T;
- var next: Node<T>;
-
- static function ListSegment(q: seq<T>, from: Node<T>, to: Node<T>, S: set<Node<T>>): bool
- reads S;
- {
- if q == []
- then from == to
- else from != null && from in S && from.data == q[0] && ListSegment(q[1..], from.next, to, S - {from})
- }
-
- static method Create(x: T) returns (l: Node<T>, ghost S: set<Node<T>>)
- ensures ListSegment([x], l, null, S) && fresh(S);
- {
- // By using the following non-deterministic 'if' statement, the example shows that 'Create' can be
- // implemented either directly or by call 'Cons'.
- if (*) {
- l := new Node<T>;
- l.data := x;
- l.next := null;
- S := {l};
- } else {
- l, S := Cons(x, null, [], {});
- }
- }
-
- static method Cons(x: T, tail: Node<T>, ghost q: seq<T>, ghost S: set<Node<T>>) returns (l: Node<T>, ghost U: set<Node<T>>)
- requires ListSegment(q, tail, null, S);
- ensures ListSegment([x] + q, l, null, U) && fresh(U - S);
- {
- l := new Node<T>;
- l.data := x;
- l.next := tail;
- U := S + {l};
- }
-}
-
-// The following class is a variation of the one above. The difference is that, in this one, each node
-// keeps track of its own contents (called 'q' above) and representation (called 'S' and 'U' above).
-class ListNode<T> {
- ghost var Contents: seq<T>;
- ghost var Repr: set<ListNode<T>>;
-
- var data: T;
- var next: ListNode<T>;
-
- static function IsList(l: ListNode<T>): bool
- reads l, l.Repr;
- {
- if l == null then
- true
- else if l.next == null then
- l in l.Repr && l.Contents == [l.data]
- else
- {l, l.next} <= l.Repr && l.Contents == [l.data] + l.next.Contents && l.next.Repr <= l.Repr - {l} && IsList(l.next)
- }
-
- static method Create(x: T) returns (l: ListNode<T>)
- ensures IsList(l) && l != null && l.Contents == [x] && fresh({l} + l.Repr);
- {
- // By using the following non-deterministic 'if' statement, the example shows that 'Create' can be
- // implemented either directly or by call 'Cons'.
- if (*) {
- l := new ListNode<T>;
- l.data := x;
- l.next := null;
- l.Repr := {l};
- l.Contents := [x];
- } else {
- l := Cons(x, null);
- }
- }
-
- static method Cons(x: T, tail: ListNode<T>) returns (l: ListNode<T>)
- requires IsList(tail);
- ensures IsList(l) && l != null;
- ensures tail == null ==> l.Contents == [x] && fresh({l} + l.Repr);
- ensures tail != null ==> l.Contents == [x] + tail.Contents && fresh({l} + l.Repr - tail.Repr);
- {
- l := new ListNode<T>;
- l.data := x;
- l.next := tail;
- if (tail != null) {
- l.Repr := tail.Repr + {l};
- l.Contents := [x] + tail.Contents;
- } else {
- l.Repr := {l};
- l.Contents := [x];
- }
- }
-}
-
-// In this final variation, a list, empty or not, is represented by a List object. The representation
-// of a List object includes a number of linked-list nodes. To make the treatment of the empty list
-// nicer than in the class above, the List object starts its list with a sentinel object whose 'data'
-// field is not used.
-class List<T>
-{
- ghost var Contents: seq<T>;
- ghost var Repr: set<object>;
- var head: LLNode<T>;
-
- function IsList(): bool
- reads this, Repr;
- {
- this in Repr && head != null && head in Repr &&
- head.Repr <= Repr && this !in head.Repr && head.IsWellFormed() &&
- Contents == head.TailContents
- }
-
- method Init()
- modifies this;
- ensures IsList() && Contents == [] && fresh(Repr - {this});
- {
- var h := new LLNode<T>;
- h.next := null;
- h.TailContents := [];
- h.Repr := {h};
-
- head := h;
- Contents := [];
- Repr := {this} + h.Repr;
- }
-
- method Cons(x: T)
- requires IsList();
- modifies Repr;
- ensures IsList() && Contents == [x] + old(Contents) && fresh(Repr - old(Repr));
- {
- head.data := x;
- assert head.IsWellFormed(); // head remains well-formed even after assigning to an object (namely, head) in head.Repr
-
- var h := new LLNode<T>;
- h.next := head;
- h.TailContents := [x] + head.TailContents;
- h.Repr := {h} + head.Repr;
-
- head := h;
- Contents := [x] + Contents;
- Repr := Repr + {h};
- }
-}
-
-class LLNode<T>
-{
- var data: T;
- var next: LLNode<T>;
- ghost var TailContents: seq<T>;
- ghost var Repr: set<object>;
-
- function IsWellFormed(): bool
- reads this, Repr;
- {
- this in Repr &&
- (next == null ==> TailContents == []) &&
- (next != null ==>
- next in Repr &&
- next.Repr <= Repr && this !in next.Repr && next.IsWellFormed() &&
- TailContents == [next.data] + next.TailContents)
- }
-}
diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy deleted file mode 100644 index ad39e3f2..00000000 --- a/Test/dafny1/Substitution.dfy +++ /dev/null @@ -1,107 +0,0 @@ -datatype List = Nil | Cons(Expr, List);
-
-datatype Expr =
- Const(int) |
- Var(int) |
- Nary(int, List);
-
-static function Subst(e: Expr, v: int, val: int): Expr
-{
- match e
- case Const(c) => e
- case Var(x) => if x == v then Expr.Const(val) else e
- case Nary(op, args) => Expr.Nary(op, SubstList(args, v, val))
-}
-
-static function SubstList(l: List, v: int, val: int): List
-{
- match l
- case Nil => l
- case Cons(e, tail) => Cons(Subst(e, v, val), SubstList(tail, v, val))
-}
-
-static ghost method Theorem(e: Expr, v: int, val: int)
- ensures Subst(Subst(e, v, val), v, val) == Subst(e, v, val);
-{
- match e {
- case Const(c) =>
- case Var(x) =>
- case Nary(op, args) =>
- Lemma(args, v, val);
- }
-}
-
-static ghost method Lemma(l: List, v: int, val: int)
- ensures SubstList(SubstList(l, v, val), v, val) == SubstList(l, v, val);
-{
- match l {
- case Nil =>
- case Cons(e, tail) =>
- Theorem(e, v, val);
- Lemma(tail, v, val);
- }
-}
-
-// -------------------------------
-
-datatype Expression =
- Const(int) |
- Var(int) |
- Nary(int, seq<Expression>);
-
-static function Substitute(e: Expression, v: int, val: int): Expression
- decreases e;
-{
- match e
- case Const(c) => e
- case Var(x) => if x == v then Expression.Const(val) else e
- case Nary(op, args) => Expression.Nary(op, SubstSeq(e, args, v, val))
-}
-
-static function SubstSeq(/*ghost*/ parent: Expression,
- q: seq<Expression>, v: int, val: int): seq<Expression>
- requires (forall a :: a in q ==> a < parent);
- decreases parent, q;
-{
- if q == [] then [] else
- SubstSeq(parent, q[..|q|-1], v, val) + [Substitute(q[|q|-1], v, val)]
-}
-
-static ghost method TheoremSeq(e: Expression, v: int, val: int)
- ensures Substitute(Substitute(e, v, val), v, val) == Substitute(e, v, val);
-{
- match e {
- case Const(c) =>
- case Var(x) =>
- case Nary(op, args) =>
- ghost var seArgs := SubstSeq(e, args, v, val);
- LemmaSeq(e, args, v, val);
-
- ghost var se := Substitute(e, v, val);
- ghost var seArgs2 := SubstSeq(se, seArgs, v, val);
- LemmaSeq(se, seArgs, v, val);
-
- var N := |args|;
- var j := 0;
- while (j < N)
- invariant j <= N;
- invariant (forall k :: 0 <= k && k < j ==> seArgs2[k] == seArgs[k]);
- {
- TheoremSeq(args[j], v, val);
- j := j + 1;
- }
- assert seArgs == seArgs2;
- }
-}
-
-static ghost method LemmaSeq(parent: Expression, q: seq<Expression>, v: int, val: int)
- requires (forall a :: a in q ==> a < parent);
- ensures |SubstSeq(parent, q, v, val)| == |q|;
- ensures (forall k :: 0 <= k && k < |q| ==>
- SubstSeq(parent, q, v, val)[k] == Substitute(q[k], v, val));
-{
- if (q == []) {
- } else {
- LemmaSeq(parent, q[..|q|-1], v, val);
- }
-}
diff --git a/Test/dafny1/SumOfCubes.dfy b/Test/dafny1/SumOfCubes.dfy deleted file mode 100644 index 7ed7ce9b..00000000 --- a/Test/dafny1/SumOfCubes.dfy +++ /dev/null @@ -1,104 +0,0 @@ -class SumOfCubes {
- static function SumEmUp(n: int, m: int): int
- requires 0 <= n && n <= m;
- decreases m - n;
- {
- if m == n then 0 else n*n*n + SumEmUp(n+1, m)
- }
-
- static method Socu(n: int, m: int) returns (r: int)
- requires 0 <= n && n <= m;
- ensures r == SumEmUp(n, m);
- {
- var a := SocuFromZero(m);
- var b := SocuFromZero(n);
- r := a - b;
- Lemma0(n, m);
- }
-
- static method SocuFromZero(k: int) returns (r: int)
- requires 0 <= k;
- ensures r == SumEmUp(0, k);
- {
- var g := Gauss(k);
- r := g * g;
- Lemma1(k);
- }
-
- ghost static method Lemma0(n: int, m: int)
- requires 0 <= n && n <= m;
- ensures SumEmUp(n, m) == SumEmUp(0, m) - SumEmUp(0, n);
- {
- var k := n;
- while (k < m)
- invariant n <= k && k <= m;
- invariant SumEmDown(0, n) + SumEmDown(n, k) == SumEmDown(0, k);
- {
- k := k + 1;
- }
- Lemma3(0, n);
- Lemma3(n, k);
- Lemma3(0, k);
- }
-
- static function GSum(k: int): int
- requires 0 <= k;
- {
- if k == 0 then 0 else GSum(k-1) + k-1
- }
-
- static method Gauss(k: int) returns (r: int)
- requires 0 <= k;
- ensures r == GSum(k);
- {
- r := k * (k - 1) / 2;
- Lemma2(k);
- }
-
- ghost static method Lemma1(k: int)
- requires 0 <= k;
- ensures SumEmUp(0, k) == GSum(k) * GSum(k);
- {
- var i := 0;
- while (i < k)
- invariant i <= k;
- invariant SumEmDown(0, i) == GSum(i) * GSum(i);
- {
- Lemma2(i);
- i := i + 1;
- }
- Lemma3(0, k);
- }
-
- ghost static method Lemma2(k: int)
- requires 0 <= k;
- ensures 2 * GSum(k) == k * (k - 1);
- {
- var i := 0;
- while (i < k)
- invariant i <= k;
- invariant 2 * GSum(i) == i * (i - 1);
- {
- i := i + 1;
- }
- }
-
- static function SumEmDown(n: int, m: int): int
- requires 0 <= n && n <= m;
- {
- if m == n then 0 else SumEmDown(n, m-1) + (m-1)*(m-1)*(m-1)
- }
-
- ghost static method Lemma3(n: int, m: int)
- requires 0 <= n && n <= m;
- ensures SumEmUp(n, m) == SumEmDown(n, m);
- {
- var k := n;
- while (k < m)
- invariant n <= k && k <= m;
- invariant SumEmUp(n, m) == SumEmDown(n, k) + SumEmUp(k, m);
- {
- k := k + 1;
- }
- }
-}
diff --git a/Test/dafny1/TerminationDemos.dfy b/Test/dafny1/TerminationDemos.dfy deleted file mode 100644 index 0aa36a10..00000000 --- a/Test/dafny1/TerminationDemos.dfy +++ /dev/null @@ -1,111 +0,0 @@ -class Example {
- method M(n: int)
- {
- var i := 0;
- while (i < n)
- {
- i := i + 1;
- }
- }
-}
-
-// -----------------------------------
-
-class Fibonacci {
- function Fib(n: int): int
- {
- if n < 2 then n else Fib(n-2) + Fib(n-1)
- }
-}
-
-// -----------------------------------
-
-class Ackermann {
- function F(m: int, n: int): int
- {
- if m <= 0 then
- n + 1
- else if n <= 0 then
- F(m - 1, 1)
- else
- F(m - 1, F(m, n - 1))
- }
-
- function G(m: int, n: int): int
- requires 0 <= m && 0 <= n;
- ensures 0 <= G(m, n);
- {
- if m == 0 then
- n + 1
- else if n == 0 then
- G(m - 1, 1)
- else
- G(m - 1, G(m, n - 1))
- }
-
- function H(m: nat, n: nat): nat
- {
- if m == 0 then
- n + 1
- else if n == 0 then
- H(m - 1, 1)
- else
- H(m - 1, H(m, n - 1))
- }
-
- method ComputeAck(m: nat, n: nat) returns (r: nat)
- {
- if (m == 0) {
- r := n + 1;
- } else if (n == 0) {
- r := ComputeAck(m - 1, 1);
- } else {
- var s := ComputeAck(m, n - 1);
- r := ComputeAck(m - 1, s);
- }
- }
-}
-
-// -----------------------------------
-
-class List {
- var data: int;
- var next: List;
- ghost var ListNodes: set<List>;
- function IsAcyclic(): bool
- reads *;
- decreases ListNodes;
- {
- this in ListNodes &&
- (next != null ==>
- next.ListNodes <= ListNodes && this !in next.ListNodes &&
- next.IsAcyclic())
- }
-
- method Singleton(x: int) returns (list: List)
- ensures list != null && list.IsAcyclic();
- {
- list := new List;
- list.data := x;
- list.next := null;
- list.ListNodes := {list};
- }
-
- method Prepend(x: int, tail: List) returns (list: List)
- requires tail == null || tail.IsAcyclic();
- ensures list != null && list.IsAcyclic();
- {
- list := new List;
- list.data := x;
- list.next := tail;
- list.ListNodes := if tail == null then {list} else {list} + tail.ListNodes;
- }
-
- function Sum(): int
- requires IsAcyclic();
- reads *;
- decreases ListNodes;
- {
- if next == null then data else data + next.Sum()
- }
-}
diff --git a/Test/dafny1/TreeDatatype.dfy b/Test/dafny1/TreeDatatype.dfy deleted file mode 100644 index a94283e6..00000000 --- a/Test/dafny1/TreeDatatype.dfy +++ /dev/null @@ -1,90 +0,0 @@ -// ------------------ generic list, non-generic tree
-
-datatype List<T> = Nil | Cons(T, List<T>);
-
-datatype Tree = Node(int, List<Tree>);
-
-static function Inc(t: Tree): Tree
-{
- match t
- case Node(n, children) => Tree.Node(n+1, ForestInc(children))
-}
-
-static function ForestInc(forest: List<Tree>): List<Tree>
-{
- match forest
- case Nil => forest
- case Cons(tree, tail) => List.Cons(Inc(tree), ForestInc(tail))
-}
-
-// ------------------ generic list, generic tree (but GInc defined only for GTree<int>
-
-datatype GTree<T> = Node(T, List<GTree<T>>);
-
-static function GInc(t: GTree<int>): GTree<int>
-{
- match t
- case Node(n, children) => GTree.Node(n+1, GForestInc(children))
-}
-
-static function GForestInc(forest: List<GTree<int>>): List<GTree<int>>
-{
- match forest
- case Nil => forest
- case Cons(tree, tail) => List.Cons(GInc(tree), GForestInc(tail))
-}
-
-// ------------------ non-generic structures
-
-datatype TreeList = Nil | Cons(OneTree, TreeList);
-
-datatype OneTree = Node(int, TreeList);
-
-static function XInc(t: OneTree): OneTree
-{
- match t
- case Node(n, children) => OneTree.Node(n+1, XForestInc(children))
-}
-
-static function XForestInc(forest: TreeList): TreeList
-{
- match forest
- case Nil => forest
- case Cons(tree, tail) => TreeList.Cons(XInc(tree), XForestInc(tail))
-}
-
-// ------------------ fun with recursive functions
-
-function len<T>(l: List<T>): int
-{
- match l
- case Nil => 0
- case Cons(h,t) => 1 + len(t)
-}
-
-function SingletonList<T>(h: T): List<T>
- ensures len(SingletonList(h)) == 1;
-{
- List.Cons(h, List.Nil)
-}
-
-function Append<T>(a: List<T>, b: List<T>): List<T>
- ensures len(Append(a,b)) == len(a) + len(b);
-{
- match a
- case Nil => b
- case Cons(h,t) => List.Cons(h, Append(t, b))
-}
-
-function Rotate<T>(n: int, l: List<T>): List<T>
- requires 0 <= n;
- ensures len(Rotate(n, l)) == len(l);
-{
- match l
- case Nil => l
- case Cons(h, t) =>
- if n == 0 then l else
- Rotate(n-1, Append(t, SingletonList(h)))
-}
-
-
diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy deleted file mode 100644 index c78d5e81..00000000 --- a/Test/dafny1/UltraFilter.dfy +++ /dev/null @@ -1,108 +0,0 @@ -// ultra filter
-
-class UltraFilter<G(==)> {
- static function IsFilter(f: set<set<G>>, S: set<G>): bool
- {
- (forall A, B :: A in f && A <= B ==> B in f) &&
- (forall C, D :: C in f && D in f ==> C * D in f) &&
- S in f &&
- {} !in f
- }
-
- static function IsUltraFilter(f: set<set<G>>, S: set<G>): bool
- {
- IsFilter(f, S) &&
- (forall g :: IsFilter(g, S) && f <= g ==> f == g)
- }
-
- method Theorem(f: set<set<G>>, S: set<G>, M: set<G>, N: set<G>)
- requires IsUltraFilter(f, S);
- requires M + N in f;
- ensures M in f || N in f;
- {
- if (M !in f) {
- // instantiate 'g' with the following 'h'
- var h := H(f, S, M);
- Lemma_HIsFilter(h, f, S, M);
- Lemma_FHOrdering0(h, f, S, M);
- }
- }
-
- // Dafny currently does not have a set comprehension expression, so this method stub will have to do
- method H(f: set<set<G>>, S: set<G>, M: set<G>) returns (h: set<set<G>>)
- ensures (forall X :: X in h <==> M + X in f);
-
- method Lemma_HIsFilter(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)
- requires IsFilter(f, S);
- requires (forall X :: X in h <==> M + X in f);
- requires M !in f;
- ensures IsFilter(h, S);
- {
- // call Lemma_H0(h, f, S, M, *, *);
- assume (forall A, B :: A in h && A <= B ==> B in h);
-
- // call Lemma_H1(h, f, S, M, *, *);
- assume (forall C, D :: C in h && D in h ==> C * D in h);
-
- Lemma_H2(h, f, S, M);
-
- Lemma_H3(h, f, S, M);
- }
-
- method Lemma_H0(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>, A: set<G>, B: set<G>)
- requires IsFilter(f, S);
- requires (forall X :: X in h <==> M + X in f);
- requires A in h && A <= B;
- ensures B in h;
- {
- assert M + A <= M + B;
- }
-
- method Lemma_H1(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>, C: set<G>, D: set<G>)
- requires IsFilter(f, S);
- requires (forall X :: X in h <==> M + X in f);
- requires C in h && D in h;
- ensures C * D in h;
- {
- assert (M + C) * (M + D) == M + (C * D);
- }
-
- method Lemma_H2(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)
- requires IsFilter(f, S);
- requires (forall X :: X in h <==> M + X in f);
- ensures S in h;
- {
- // S is intended to stand for the universal set, but this is the only place where that plays a role
- assume M <= S;
-
- assert M + S == S;
- }
-
- method Lemma_H3(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)
- requires IsFilter(f, S);
- requires (forall X :: X in h <==> M + X in f);
- requires M !in f;
- ensures {} !in h;
- {
- assert M + {} == M;
- }
-
- method Lemma_FHOrdering0(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)
- requires IsFilter(f, S);
- requires (forall X :: X in h <==> M + X in f);
- requires IsFilter(h, S);
- ensures f <= h;
- {
- // call Lemma_FHOrdering1(h, f, S, M, *);
- assume (forall Y :: Y in f ==> Y in h);
- assume f <= h; // hickup in boxing
- }
-
- method Lemma_FHOrdering1(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>, Y: set<G>)
- requires IsFilter(f, S);
- requires (forall X :: X in h <==> M + X in f);
- ensures Y in f ==> Y in h;
- {
- assert Y <= M + Y;
- }
-}
diff --git a/Test/dafny1/UnboundedStack.dfy b/Test/dafny1/UnboundedStack.dfy deleted file mode 100644 index dfc10327..00000000 --- a/Test/dafny1/UnboundedStack.dfy +++ /dev/null @@ -1,96 +0,0 @@ -class UnboundedStack<T> {
- ghost var representation: set<object>;
- ghost var content: seq<T>;
- var top: Node<T>;
-
- function IsUnboundedStack(): bool
- reads this, representation;
- {
- this in representation &&
- (top == null ==>
- content == []) &&
- (top != null ==>
- top in representation && this !in top.footprint && top.footprint <= representation &&
- content == top.content &&
- top.Valid())
- }
-
- method InitUnboundedStack()
- modifies this;
- ensures IsUnboundedStack();
- ensures content == [];
- {
- this.top := null;
- this.content := [];
- this.representation := {this};
- }
-
- method Push(val: T)
- requires IsUnboundedStack();
- modifies this;
- ensures IsUnboundedStack();
- ensures content == [val] + old(content);
- {
- top := new Node<T>.InitNode(val,top);
- representation := representation + top.footprint;
- content := [val] + content;
- }
-
- method Pop() returns (result: T)
- requires IsUnboundedStack();
- requires content != [];
- modifies this;
- ensures IsUnboundedStack();
- ensures content == old(content)[1..];
- {
- result := top.val;
- top := top.next;
- content := content[1..];
- }
-
- method isEmpty() returns (result: bool)
- requires IsUnboundedStack();
- ensures result <==> content == [];
- {
- result := top == null;
- }
-}
-
-class Node<T> {
- ghost var footprint: set<object>;
- ghost var content: seq<T>;
- var val: T;
- var next: Node<T>;
-
- function Valid(): bool
- reads this, footprint;
- {
- this in footprint &&
- (next == null ==>
- content == [val]) &&
- (next != null ==>
- next in footprint && next.footprint <= footprint && this !in next.footprint &&
- content == [val] + next.content &&
- next.Valid())
- }
-
- method InitNode(val: T, next: Node<T>)
- requires next != null ==> next.Valid() && !(this in next.footprint);
- modifies this;
- ensures Valid();
- ensures next != null ==> content == [val] + next.content &&
- footprint == {this} + next.footprint;
- ensures next == null ==> content == [val] &&
- footprint == {this};
- {
- this.val := val;
- this.next := next;
- if (next == null) {
- this.footprint := {this};
- this.content := [val];
- } else {
- this.footprint := {this} + next.footprint;
- this.content := [val] + next.content;
- }
- }
-}
diff --git a/Test/dafny1/pow2.dfy b/Test/dafny1/pow2.dfy deleted file mode 100644 index c7e4bc63..00000000 --- a/Test/dafny1/pow2.dfy +++ /dev/null @@ -1,54 +0,0 @@ -// This is a Dafny adaptation of a Coq program by David Pichardie.
-
-function IsEven(n: int): bool
- requires 0 <= n;
- ensures IsEven(n) ==> n == (n/2)+(n/2);
-{
- (n/2)*2 == n
-}
-
-function Square(n: int): int { n * n }
-
-function pow2(n: int): int
- requires 0 <= n;
- ensures 0 <= pow2(n);
-{
- if n == 0 then
- 1
- else if IsEven(n) then
- Square(pow2(n / 2))
- else
- 2*pow2(n-1)
-
-}
-
-function pow2_slow(n: int): int
- requires 0 <= n;
-{
- if n == 0 then
- 1
- else
- 2*pow2_slow(n-1)
-}
-
-ghost method Lemma(n: int)
- requires 0 <= n && IsEven(n);
- ensures pow2_slow(n) == Square(pow2_slow(n/2));
-{
- if (n != 0) {
- Lemma(n-2);
- }
-}
-
-ghost method Theorem(n: int)
- requires 0 <= n;
- ensures pow2(n) == pow2_slow(n);
-{
- if (n == 0) {
- } else if (IsEven(n)) {
- Lemma(n);
- Theorem(n/2);
- } else {
- Theorem(n-1);
- }
-}
diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat deleted file mode 100644 index a49bbf9a..00000000 --- a/Test/dafny1/runtest.bat +++ /dev/null @@ -1,23 +0,0 @@ -@echo off
-setlocal
-
-set BOOGIEDIR=..\..\Binaries
-set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
-
-for %%f in (Queue.dfy PriorityQueue.dfy
- ExtensibleArray.dfy ExtensibleArrayAuto.dfy
- BinaryTree.dfy
- UnboundedStack.dfy
- SeparationLogicList.dfy
- ListCopy.dfy ListReverse.dfy ListContents.dfy
- MatrixFun.dfy pow2.dfy
- SchorrWaite.dfy SchorrWaite-stages.dfy
- Cubes.dfy SumOfCubes.dfy FindZero.dfy
- TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy
- Induction.dfy Rippling.dfy MoreInduction.dfy
- Celebrity.dfy BDD.dfy
- UltraFilter.dfy) do (
- echo.
- echo -------------------- %%f --------------------
- %DAFNY_EXE% /compile:0 /vcsMaxKeepGoingSplits:2 /dprint:out.dfy.tmp %* %%f
-)
|