diff options
| -rw-r--r-- | Test/VSI-Benchmarks/Answer | 28 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b1.dfy | 47 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b2.dfy | 60 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b3.dfy | 151 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b4.dfy | 119 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b5.dfy | 205 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b6.dfy | 139 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b7.dfy | 166 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b8.dfy | 375 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/runtest.bat | 14 |
10 files changed, 1304 insertions, 0 deletions
diff --git a/Test/VSI-Benchmarks/Answer b/Test/VSI-Benchmarks/Answer new file mode 100644 index 00000000..0149855c --- /dev/null +++ b/Test/VSI-Benchmarks/Answer @@ -0,0 +1,28 @@ +
+-------------------- b1.dfy --------------------
+
+Dafny program verifier finished with 2 verified, 0 errors
+
+-------------------- b2.dfy --------------------
+
+Dafny program verifier finished with 3 verified, 0 errors
+
+-------------------- b3.dfy --------------------
+
+Dafny program verifier finished with 4 verified, 0 errors
+
+-------------------- b4.dfy --------------------
+
+Dafny program verifier finished with 6 verified, 0 errors
+
+-------------------- b5.dfy --------------------
+
+Dafny program verifier finished with 12 verified, 0 errors
+
+-------------------- b6.dfy --------------------
+
+Dafny program verifier finished with 12 verified, 0 errors
+
+-------------------- b7.dfy --------------------
+
+Dafny program verifier finished with 11 verified, 0 errors
diff --git a/Test/VSI-Benchmarks/b1.dfy b/Test/VSI-Benchmarks/b1.dfy new file mode 100644 index 00000000..ba293008 --- /dev/null +++ b/Test/VSI-Benchmarks/b1.dfy @@ -0,0 +1,47 @@ +// Note: To prove termination of calls, methods need
+// a termination measure, but Dafny does not yet support
+// termination measures for methods (but it will in
+// the foreseeable future).
+
+// Spec# and Boogie and Chalice: The program will be
+// the same, except that these languages do not check
+// for any kind of termination.
+
+class Benchmark1 {
+ method Add(x: int, y: int) returns (r: int)
+ ensures r == x+y;
+ {
+ r := x;
+ if (y < 0) {
+ var n := y;
+ while (n != 0)
+ invariant r == x+y-n && 0 <= -n;
+ decreases -n;
+ {
+ r := r - 1;
+ n := n + 1;
+ }
+ } else {
+ var n := y;
+ while (n != 0)
+ invariant r == x+y-n && 0 <= n;
+ decreases n;
+ {
+ r := r + 1;
+ n := n - 1;
+ }
+ }
+ }
+
+ method Mul(x: int, y: int) returns (r: int)
+ ensures r == x*y;
+ {
+ if (x < 0) {
+ call r := Mul(-x, y);
+ r := -r;
+ } else {
+ call r := Mul(x-1, y);
+ call r := Add(r, y);
+ }
+ }
+}
diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy new file mode 100644 index 00000000..53eb49a8 --- /dev/null +++ b/Test/VSI-Benchmarks/b2.dfy @@ -0,0 +1,60 @@ +
+// Note: There is a bug in the well-formedness of functions. In particular,
+// it doesn't look at the requires clause (in the proper way). Fixed!
+// Note:Implemented arrays as Dafny does not provide them
+
+class Benchmark2 {
+ method BinarySearch(a: Array, key: int) returns (result: int)
+ requires a != null;
+ requires (forall i, j ::
+ 0 <= i && i < j && j < a.Length() ==> a.Get(i) <= a.Get(j));
+ ensures -1 <= result && result < a.Length();
+ ensures 0 <= result ==> a.Get(result) == key;
+ ensures result == -1 ==>
+ (forall i :: 0 <= i && i < a.Length() ==> a.Get(i) != key);
+ {
+ var low := 0;
+ var high := a.Length();
+
+ while (low < high)
+ invariant 0 <= low && high <= a.Length();
+ invariant (forall i :: 0 <= i && i < low ==> a.Get(i) < key);
+ invariant (forall i :: high <= i && i < a.Length() ==> key < a.Get(i));
+ decreases high - low;
+ {
+ var mid := low + (high - low) / 2;
+ var midVal := a.Get(mid);
+
+ if (midVal < key) {
+ low := mid + 1;
+ } else if (key < midVal) {
+ high := mid;
+ } else {
+ result := mid; // key found
+ return;
+ }
+ }
+ result := -1; // key not present
+ }
+}
+
+class Array {
+ var contents: seq<int>;
+ method Init(n: int);
+ requires 0 <= n;
+ modifies this;
+ ensures |contents| == n;
+ function Length(): int
+ reads this;
+ { |contents| }
+ function Get(i: int): int
+ requires 0 <= i && i < |contents|;
+ reads this;
+ { contents[i] }
+ method Set(i: int, x: int);
+ requires 0 <= i && i < |contents|;
+ modifies this;
+ ensures contents[..i] == old(contents[..i]);
+ ensures contents[i] == x;
+ ensures contents[i+1..] == old(contents[i+1..]);
+}
diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy new file mode 100644 index 00000000..a11dec52 --- /dev/null +++ b/Test/VSI-Benchmarks/b3.dfy @@ -0,0 +1,151 @@ +// Note: We used integers instead of a generic Comparable type, because
+// Dafny has no way of saying that the Comparable type's AtMost function
+// is total and transitive.
+
+// Note: We couldn't get things to work out if we used the Get method.
+// Instead, we used .contents.
+
+// Note: Due to infelicities of the Dafny sequence treatment, we
+// needed to supply two lemmas, do a complicated assignment of
+// pperm, had to write invariants over p and perm rather than pperm and we couldn't use
+// "x in p".
+
+//would be nice if we could mark pperm as a ghost variable
+
+class Queue<T> {
+ var contents: seq<int>;
+ method Init();
+ modifies this;
+ ensures |contents| == 0;
+ method Enqueue(x: int);
+ modifies this;
+ ensures contents == old(contents) + [x];
+ method Dequeue() returns (x: int);
+ requires 0 < |contents|;
+ modifies this;
+ ensures contents == old(contents)[1..] && x == old(contents)[0];
+ function Head(): int
+ requires 0 < |contents|;
+ reads this;
+ { contents[0] }
+ function Get(i: int): int
+ requires 0 <= i && i < |contents|;
+ reads this;
+ { contents[i] }
+}
+
+class Comparable {
+ function AtMost(c: Comparable): bool;
+ reads this, c;
+}
+
+
+class Benchmark3 {
+
+
+ method Sort(q: Queue<int>) returns (r: Queue<int>, perm:seq<int>)
+ requires q != null;
+ modifies q;
+ ensures r != null && fresh(r);
+ ensures |r.contents| == |old(q.contents)|;
+ ensures (forall i, j :: 0 <= i && i < j && j < |r.contents| ==>
+ r.Get(i) <= r.Get(j));
+ //perm is a permutation
+ ensures |perm| == |r.contents|; // ==|pperm|
+ ensures (forall i: int :: 0 <= i && i < |perm|==> 0 <= perm[i] && perm[i] < |perm| );
+ ensures (forall i, j: int :: 0 <= i && i < j && j < |perm| ==> perm[i] != perm[j]);
+ // the final Queue is a permutation of the input Queue
+ ensures (forall i: int :: 0 <= i && i < |perm| ==> r.contents[i] == old(q.contents)[perm[i]]);
+ {
+ r := new Queue<int>;
+ call r.Init();
+ var p:= [];
+
+ var n := 0;
+ while (n < |q.contents|)
+ invariant n <=|q.contents| ;
+ invariant (forall i: int :: 0 <= i && i < n ==> p[i] == i);
+ invariant n == |p|;
+ decreases |q.contents| -n;
+ {
+ p := p + [n];
+ n := n + 1;
+ }
+ perm:= [];
+ var pperm := p + perm;
+
+ while (|q.contents| != 0)
+ invariant |r.contents| == |old(q.contents)| - |q.contents|;
+ invariant (forall i, j :: 0 <= i && i < j && j < |r.contents| ==>
+ r.contents[i] <= r.contents[j]);
+ invariant (forall i, j ::
+ 0 <= i && i < |r.contents| &&
+ 0 <= j && j < |q.contents|
+ ==> r.contents[i] <= q.contents[j]);
+
+ // pperm is a permutation
+ invariant pperm == p + perm && |p| == |q.contents| && |perm| == |r.contents|;
+ invariant (forall i: int :: 0 <= i && i < |perm| ==> 0 <= perm[i] && perm[i] < |pperm|);
+ invariant (forall i: int :: 0 <= i && i < |p| ==> 0 <= p[i] && p[i] < |pperm|);
+ invariant (forall i, j: int :: 0 <= i && i < j && j < |pperm| ==> pperm[i] != pperm[j]);
+ // the current array is that permutation of the input array
+ invariant (forall i: int :: 0 <= i && i < |perm| ==> r.contents[i] == old(q.contents)[perm[i]]);
+ invariant (forall i: int :: 0 <= i && i < |p| ==> q.contents[i] == old(q.contents)[p[i]]);
+
+ decreases |q.contents|;
+ {
+ var m,k;
+ call m,k := RemoveMin(q);
+ perm := perm + [p[k]]; //adds index of min to perm
+ p := p[k+1..]+ p[..k]; //remove index of min from p
+ call r.Enqueue(m);
+ pperm:= pperm[k+1..|p|+1] + pperm[..k] + pperm[|p|+1..] +[pperm[k]];
+ }
+ assert (forall i:int :: 0<=i && i < |perm| ==> perm[i] == pperm[i]); //needed to trigger axiom
+ }
+
+
+
+ method RemoveMin(q: Queue<int>) returns (m: int, k:int) //m is the min, k is m's index in q
+ requires q != null && |q.contents| != 0;
+ modifies q;
+ ensures |old(q.contents)| == |q.contents| + 1;
+ ensures 0 <= k && k < |old(q.contents)| && old(q.contents[k]) == m;
+ ensures (forall i :: 0 <= i && i < |q.contents| ==> m <= q.contents[i]);
+ ensures q.contents == old(q.contents)[k+1..] + old(q.contents)[..k];
+ {
+ var n := |q.contents|;
+ k := 0;
+ m := q.Head();
+ var j := 0;
+
+ while (j <n)
+ invariant j <= n;
+ invariant q.contents == old(q.contents)[j..] + old(q.contents)[..j]; //i.e. rotated
+ invariant 0 <= k && k < |old(q.contents)| && old(q.contents)[k] == m;
+ invariant (forall i ::0<= i && i < j ==> m <= old(q.contents)[i]); //m is min so far
+ decreases n-j;
+ {
+ var x;
+ call x:= q.Dequeue();
+ call q.Enqueue(x);
+ if ( x < m) {k := j; m := x;}
+ j:= j+1;
+
+ }
+
+ j := 0;
+ while (j < k)
+ invariant j <= k;
+ invariant q.contents == old(q.contents)[j..] + old(q.contents)[..j];
+ decreases k-j;
+ {
+ var x;
+ call x := q.Dequeue();
+ call q.Enqueue(x);
+ j:= j +1;
+ }
+
+ call m:= q.Dequeue();
+ }
+}
diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy new file mode 100644 index 00000000..b0b370a0 --- /dev/null +++ b/Test/VSI-Benchmarks/b4.dfy @@ -0,0 +1,119 @@ +// Note: We are using the built-in equality to compare keys.
+// Note: Our specifications are rather tied to the implementation. In
+// particular, we use indices into .keys and .values. Nicer would
+// be if Dafny had a built-in map type that could be used in specifications.
+// Or, perhaps inductive data types could be used in specifications,
+// if Dafny had those.
+
+class Map<Key,Value> {
+ var keys: seq<Key>;
+ var values: seq<Value>;
+
+ function Valid(): bool
+ reads this;
+ {
+ |keys| == |values| &&
+ (forall i, j :: 0 <= i && i < j && j < |keys| ==> keys[i] != keys[j])
+ }
+
+ method Init()
+ modifies this;
+ ensures Valid() && |keys| == 0;
+ {
+ keys := [];
+ values := [];
+ }
+
+ method Find(key: Key) returns (present: bool, val: Value)
+ requires Valid();
+ ensures !present ==> !(key in keys);
+ ensures present ==> (exists i :: 0 <= i && i < |keys| &&
+ keys[i] == key && values[i] == val);
+ {
+ var j;
+ call j := FindIndex(key);
+ if (j == -1) {
+ present := false;
+ } else {
+ present := true;
+ val := values[j];
+ }
+ }
+
+ method Add(key: Key, val: Value)
+ requires Valid();
+ modifies this;
+ ensures Valid();
+ // no key is lost:
+ ensures (forall k :: k in old(keys) ==> k in keys);
+ // at most one key is introduced:
+ ensures (forall k :: k in keys ==> k in old(keys) || k == key);
+ // the given key has the given value:
+ ensures (exists i :: 0 <= i && i < |keys| &&
+ keys[i] == key && values[i] == val);
+ // other values don't change:
+ ensures (forall i :: 0 <= i && i < |keys| && keys[i] != key ==>
+ values[i] == old(values)[i]);
+ {
+ var j;
+ call j := FindIndex(key);
+ if (j == -1) {
+ keys := keys + [key];
+ values := values + [val];
+ assert values[|keys|-1] == val; // lemma
+ } else {
+ keys := keys[..j] + [key] + keys[j+1..];
+ values := values[..j] + [val] + values[j+1..];
+ assert values[j] == val; //lemma
+ }
+ }
+
+ method Remove(key: Key)
+ requires Valid();
+ modifies this;
+ ensures Valid();
+ // no key is introduced:
+ ensures (forall k :: k in keys ==> k in old(keys));
+ // at most one key is removed:
+ ensures (forall k :: k in old(keys) ==> k in keys || k == key);
+ // the given key is not there:
+ // other values don't change:
+ ensures !(key in old(keys)) ==> keys == old(keys) && values == old(values);
+ ensures key in old(keys) ==>
+ !(key in keys) &&
+ (exists h ::
+ 0 <= h && h <= |keys| &&
+ keys[..h] == old(keys)[..h] &&
+ values[..h] == old(values)[..h] &&
+ keys[h..] == old(keys)[h+1..] &&
+ values[h..] == old(values)[h+1..]);
+ {
+ var j;
+ call j := FindIndex(key);
+ if (0 <= j) {
+ keys := keys[..j] + keys[j+1..];
+ values := values[..j] + values[j+1..];
+ }
+ }
+
+ method FindIndex(key: Key) returns (idx: int)
+ requires Valid();
+ ensures -1 <= idx && idx < |keys|;
+ ensures idx == -1 ==> !(key in keys);
+ ensures 0 <= idx ==> keys[idx] == key;
+ {
+ var j := 0;
+ while (j < |keys|)
+ invariant j <= |keys|;
+ invariant !(key in keys[..j]);
+ decreases |keys| -j;
+ {
+ if (keys[j] == key) {
+ idx := j;
+ return;
+ }
+ j := j + 1;
+ }
+ idx := -1;
+ }
+}
diff --git a/Test/VSI-Benchmarks/b5.dfy b/Test/VSI-Benchmarks/b5.dfy new file mode 100644 index 00000000..9d384c38 --- /dev/null +++ b/Test/VSI-Benchmarks/b5.dfy @@ -0,0 +1,205 @@ +
+
+class Queue<T> {
+ var head: Node<T>;
+ var tail: Node<T>;
+
+ var contents: seq<T>;
+ var footprint: set<object>;
+ 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.Valid() &&
+ n.footprint <= footprint &&
+ (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>;
+ call n.Init();
+ head := n;
+ tail := n;
+ contents := n.tailContents;
+ footprint := {this} + n.footprint;
+ spine := {n};
+ }
+
+ 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>;
+ call n.Init(); n.data := t;
+ tail.next := n;
+ tail := n;
+
+ foreach (m in spine) {
+ m.tailContents := m.tailContents + [t];
+ }
+ contents := head.tailContents;
+
+ foreach (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;
+ }
+
+
+ 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: T;
+ call t := Front();
+ call Dequeue();
+ call Enqueue(t);
+ }
+
+ method RotateAny()
+ requires Valid();
+ requires 0 < |contents|;
+ modifies footprint;
+ ensures Valid() && fresh(footprint - old(footprint));
+ ensures (exists i :: 0 <= i && i <= |contents| &&
+ contents == old(contents)[i..] + old(contents)[..i]);
+ {
+ var t: T;
+ call t := Front();
+ call Dequeue();
+ call Enqueue(t);
+ }
+
+}
+
+class Node<T> {
+ var data: T;
+ var next: Node<T>;
+
+ var tailContents: seq<T>;
+ 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>;
+ call q0.Init();
+ var q1 := new Queue<T>;
+ call q1.Init();
+
+ call q0.Enqueue(t);
+ call q0.Enqueue(u);
+
+ call q1.Enqueue(v);
+
+ assert |q0.contents| == 2;
+
+ var w;
+ call w := q0.Front();
+ assert w == t;
+ call q0.Dequeue();
+
+ call 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));
+ {
+ call q0.Enqueue(t);
+ call q0.Enqueue(u);
+
+ call q1.Enqueue(v);
+
+ assert |q0.contents| == 2;
+
+ var w;
+ call w := q0.Front();
+ assert w == t;
+ call q0.Dequeue();
+
+ call w := q0.Front();
+ assert w == u;
+
+ assert |q0.contents| == 1;
+ assert |q1.contents| == old(|q1.contents|) + 1;
+ }
+}
diff --git a/Test/VSI-Benchmarks/b6.dfy b/Test/VSI-Benchmarks/b6.dfy new file mode 100644 index 00000000..e5d061d2 --- /dev/null +++ b/Test/VSI-Benchmarks/b6.dfy @@ -0,0 +1,139 @@ +
+class Collection {
+ var footprint:set<object>;
+ var elements:seq<int>;
+
+ function Valid():bool
+ reads this, footprint;
+ {
+ this in footprint
+ }
+
+ method GetCount() returns (c:int)
+ requires Valid();
+ ensures 0<=c;
+ {
+ c:=|elements|;
+ }
+
+ method Init()
+ modifies this;
+ ensures Valid() && fresh(footprint -{this});
+ {
+ elements := [];
+ footprint := {this};
+ }
+
+ method GetItem(i:int ) returns (x:int)
+ requires Valid();
+ requires 0<=i && i<|elements|;
+ ensures elements[i] ==x;
+ {
+ x:=elements[i];
+ }
+
+ method Add(x:int )
+ requires Valid();
+ modifies footprint;
+ ensures Valid() && fresh(footprint - old(footprint));
+ ensures elements == old(elements) + [x];
+ {
+ elements:= elements + [x];
+ }
+
+ method GetIterator() returns (iter:Iterator)
+ requires Valid();
+ ensures iter != null && iter.Valid();
+ ensures fresh(iter.footprint) && iter.pos == -1;
+ ensures iter.c == this;
+ {
+ iter:= new Iterator;
+ call iter.Init(this);
+ }
+
+}
+
+class Iterator {
+
+ var c:Collection;
+ var pos:int;
+
+ var footprint:set<object>;
+
+ function Valid():bool
+ reads this, footprint;
+ {
+ this in footprint && c!= null && -1<= pos && !(null in footprint)
+ }
+
+ method Init(coll:Collection)
+ requires coll != null;
+ modifies this;
+ ensures Valid() && fresh(footprint -{this}) && pos ==-1;
+ ensures c == coll;
+ {
+ c:= coll;
+ pos:=-1;
+ footprint := {this};
+ }
+
+ method MoveNext() returns (b:bool)
+ requires Valid();
+ modifies footprint;
+ ensures fresh(footprint - old(footprint)) && Valid() && pos == old(pos) + 1;
+ ensures b == HasCurrent() && c == old(c);
+ {
+ pos:= pos+1;
+ b:= pos < |c.elements|;
+ }
+
+ function HasCurrent():bool //???
+ requires Valid();
+ reads this, c;
+ {
+ 0<= pos && pos < |c.elements|
+ }
+
+ method GetCurrent() returns (x:int)
+ requires Valid() && HasCurrent();
+ ensures c.elements[pos] == x;
+ {
+ x:=c.elements[pos];
+ }
+
+}
+
+class Client
+{
+
+ method Main()
+ {
+ var c:= new Collection;
+ call c.Init();
+ call c.Add(33);
+ call c.Add(45);
+ call c.Add(78);
+
+ var iter,b,x, s:= [ ];
+
+ call iter:=c.GetIterator();
+ call b:= iter.MoveNext();
+
+ while (b)
+ invariant b == iter.HasCurrent() && fresh(iter.footprint) && iter.Valid();
+ invariant c.Valid() && fresh(c.footprint) && iter.footprint !! c.footprint; //disjoint footprints
+ invariant 0<= iter.pos && iter.pos <=|c.elements| && s == c.elements[..iter.pos] ;
+ invariant iter.c == c;
+ decreases |c.elements| - iter.pos;
+ {
+ call x:= iter.GetCurrent();
+ s:= s + [x];
+ call b:= iter.MoveNext();
+ }
+
+ assert s == c.elements; //verifies that the iterator returns the correct things
+ call c.Add(100);
+ }
+
+}
+
diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy new file mode 100644 index 00000000..13a8ccd2 --- /dev/null +++ b/Test/VSI-Benchmarks/b7.dfy @@ -0,0 +1,166 @@ +// Edited B6 to include GetChar and PutChar
+
+//This is the Queue from Benchmark 3.
+
+//restriction:we assume streams are finite
+//what else can we specify?
+
+
+class Queue<T> {
+ var contents: seq<int>;
+ method Init();
+ modifies this;
+ ensures |contents| == 0;
+ method Enqueue(x: int);
+ modifies this;
+ ensures contents == old(contents) + [x];
+ method Dequeue() returns (x: int);
+ requires 0 < |contents|;
+ modifies this;
+ ensures contents == old(contents)[1..] && x == old(contents)[0];
+ function Head(): int
+ requires 0 < |contents|;
+ reads this;
+ { contents[0] }
+ function Get(i: int): int
+ requires 0 <= i && i < |contents|;
+ reads this;
+ { contents[i] }
+}
+
+class Stream {
+ var footprint:set<object>;
+ var stream:seq<int>;
+ var isOpen:bool;
+
+ function Valid():bool
+ reads this, footprint;
+ {
+ !(null in footprint) && this in footprint && isOpen
+ }
+
+ method GetCount() returns (c:int)
+ requires Valid();
+ ensures 0<=c;
+ {
+ c:=|stream|;
+ }
+
+ method Create() //writing
+ modifies this;
+ ensures Valid() && fresh(footprint -{this});
+ ensures stream == [];
+ {
+ stream := [];
+ footprint := {this};
+ isOpen:= true;
+ }
+
+ method Open() //reading
+ modifies this;
+ ensures Valid() && fresh(footprint -{this});
+ {
+ footprint := {this};
+ isOpen :=true;
+ }
+
+ method PutChar(x:int )
+ requires Valid();
+ modifies footprint;
+ ensures Valid() && fresh(footprint - old(footprint));
+ ensures stream == old(stream) + [x];
+ {
+ stream:= stream + [x];
+ }
+
+ method GetChar()returns(x:int)
+ requires Valid() && 0< |stream|;
+ modifies footprint;
+ ensures Valid() && fresh(footprint - old(footprint));
+ ensures x ==old(stream)[0];
+ ensures stream == old(stream)[1..];
+ {
+ x := stream[0];
+ stream:= stream[1..];
+
+ }
+
+ method AtEndOfStream() returns(eos:bool)
+ requires Valid();
+ ensures eos <==> |stream| ==0;
+ {
+ eos:= |stream| ==0;
+ }
+
+ method Close()
+ requires Valid();
+ modifies footprint;
+ {
+ isOpen := false;
+
+ }
+
+}
+
+
+
+class Client {
+
+
+ method Sort(q: Queue<int>) returns (r: Queue<int>, perm:seq<int>);
+ requires q != null;
+ modifies q;
+ ensures r != null && fresh(r);
+ ensures |r.contents| == |old(q.contents)|;
+ ensures (forall i, j :: 0 <= i && i < j && j < |r.contents| ==>
+ r.Get(i) <= r.Get(j));
+ //perm is a permutation
+ ensures |perm| == |r.contents|; // ==|pperm|
+ ensures (forall i: int :: 0 <= i && i < |perm|==> 0 <= perm[i] && perm[i] < |perm| );
+ ensures (forall i, j: int :: 0 <= i && i < j && j < |perm| ==> perm[i] != perm[j]);
+ // the final Queue is a permutation of the input Queue
+ ensures (forall i: int :: 0 <= i && i < |perm| ==> r.contents[i] == old(q.contents)[perm[i]]);
+
+
+
+ method Main()
+ {
+ var rd:= new Stream;
+ call rd.Open();
+
+ var q:= new Queue<int>;
+ var ch;
+ while (true)
+ invariant rd.Valid() && fresh(rd.footprint) && fresh(q);
+ decreases |rd.stream|;
+ {
+ var eos:bool;
+ call eos := rd.AtEndOfStream();
+ if (eos)
+ {
+ break;
+ }
+
+ call ch := rd.GetChar();
+ call q.Enqueue(ch);
+ }
+
+ call rd.Close();
+ var perm;
+ call q,perm := Sort(q);
+
+ var wr:= new Stream;
+ call wr.Create();
+ while (0<|q.contents|)
+ invariant wr.Valid() && fresh(wr.footprint) && fresh(q) && !(q in wr.footprint);
+ decreases |q.contents|;
+ {
+ call ch:= q.Dequeue();
+ call wr.PutChar(ch);
+ }
+ call wr.Close();
+
+ }
+
+}
+
diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy new file mode 100644 index 00000000..01b10a5a --- /dev/null +++ b/Test/VSI-Benchmarks/b8.dfy @@ -0,0 +1,375 @@ +// Benchmark 8
+
+// A dictionary is a mapping between words and sequences of words
+// to set up the dictionary in main we will read a stream of words and put them into the mapping - the first element of the stream is the term,
+// the following words (until we read null) form the terms definition. Then the stream provides the next term etc.
+
+class Queue<T> {
+ var contents: seq<Word>;
+ method Init();
+ modifies this;
+ ensures |contents| == 0;
+ method Enqueue(x: Word);
+ modifies this;
+ ensures contents == old(contents) + [x];
+ method Dequeue() returns (x: Word);
+ requires 0 < |contents|;
+ modifies this;
+ ensures contents == old(contents)[1..] && x == old(contents)[0];
+ function Head(): Word
+ requires 0 < |contents|;
+ reads this;
+ { contents[0] }
+ function Get(i: int): Word
+ requires 0 <= i && i < |contents|;
+ reads this;
+ { contents[i] }
+}
+
+
+class Glossary {
+
+
+ method Sort(q: Queue<Word>) returns (r: Queue<Word>, perm:seq<int>);
+ requires q != null;
+ modifies q;
+ ensures r != null && fresh(r);
+ ensures |r.contents| == |old(q.contents)|;
+ ensures (forall i, j :: 0 <= i && i < j && j < |r.contents| ==>
+ r.Get(i).AtMost(r.Get(j)));
+ //perm is a permutation
+ ensures |perm| == |r.contents|; // ==|pperm|
+ ensures (forall i: int :: 0 <= i && i < |perm|==> 0 <= perm[i] && perm[i] < |perm| );
+ ensures (forall i, j: int :: 0 <= i && i < j && j < |perm| ==> perm[i] != perm[j]);
+ // the final Queue is a permutation of the input Queue
+ ensures (forall i: int :: 0 <= i && i < |perm| ==> r.contents[i] == old(q.contents)[perm[i]]);
+
+
+
+ method main()
+ {
+ var rs:= new ReaderStream;
+ call rs.Open();
+ var glossary := new Map<Word,seq<Word>>;
+ call glossary.Init();
+ var q:= new Queue<Word>;
+ call q.Init();
+
+ while (true)
+ invariant rs.Valid() && fresh(rs.footprint);
+ invariant glossary.Valid();
+ invariant !(glossary in rs.footprint);
+ invariant !(null in glossary.keys);
+ //to do add invariant invariant (forall d:: d in glossary.values ==>!(null in d)); ***
+ invariant !(q in rs.footprint);
+ // ** invariant q.contents == glossary.keys; need a quantifer to express this (map doesnt necessarily add to end)
+ // we leave out the decreases clause - unbounded stream
+ {
+ var term,definition;
+ call term,definition := readDefinition(rs);
+ if (term == null)
+ {
+ break;
+ }
+ call glossary.Add(term,definition);
+ call q.Enqueue(term);
+ }
+
+ call rs.Close();
+ var p;
+ call q,p := Sort(q);
+ var wr := new WriterStream;
+ call wr.Create();
+
+ while (0<|q.contents|)
+ invariant wr.Valid() && fresh(wr.footprint);
+ invariant glossary.Valid();
+ invariant !(glossary in wr.footprint);
+ invariant !(null in glossary.keys);
+ invariant !(q in wr.footprint);
+ decreases |q.contents|;
+ {
+ var term, present, definition;
+ call term:= q.Dequeue();
+ call present,definition:= glossary.Find(term);
+ assume present; // to change this into an assert we need the loop invariant ** above that we commented out
+
+ // write term with a html anchor
+ call wr.PutWordInsideTag(term, term);
+ var i := 0;
+
+ while ( i < |definition|)
+ invariant wr.Valid() && fresh(wr.footprint);
+ invariant !(glossary in wr.footprint);
+ invariant !(q in wr.footprint);
+ decreases |definition| -i;
+ {
+ var w := definition[i];
+ var d;
+ assume w != null; // to convert this into an assert we need invariant *** above
+ call present, d := glossary.Find(w);
+ if (present)
+ {
+ call wr. PutWordInsideHyperlink(w, w);
+ }
+ else
+ {
+ call wr. PutWord(w);
+ }
+ i:= i +1;
+ }
+ }
+ call wr.Close();
+ }
+
+
+ method readDefinition(rs:ReaderStream) returns (term:Word, definition:seq<Word>)
+ requires rs != null && rs.Valid();
+ modifies rs.footprint;
+ ensures rs.Valid() && fresh(rs.footprint - old(rs.footprint));
+ ensures term != null ==> !(null in definition);
+ {
+ call term := rs.GetWord();
+ if (term != null)
+ {
+ definition := [];
+ while (true)
+ invariant rs.Valid() && fresh(rs.footprint - old(rs.footprint));
+ invariant !(null in definition);
+ {
+ var w;
+ call w := rs.GetWord();
+ if (w == null)
+ {
+ break;
+ }
+ definition := definition + [w];
+ }
+ }
+
+ }
+
+ }
+
+ class Word
+ {
+
+ function AtMost(w:Word) :bool;
+
+ }
+
+ class ReaderStream {
+ var footprint:set<object>;
+ var isOpen:bool;
+
+ function Valid():bool
+ reads this, footprint;
+ {
+ !(null in footprint) && this in footprint && isOpen
+ }
+
+ method Open() //reading
+ modifies this;
+ ensures Valid() && fresh(footprint -{this});
+ {
+ footprint := {this};
+ isOpen :=true;
+ }
+
+ method GetWord()returns(x:Word)
+ requires Valid() ;
+ modifies footprint;
+ ensures Valid() && fresh(footprint - old(footprint));
+ {
+
+ }
+
+ method Close()
+ requires Valid();
+ modifies footprint;
+ {
+ isOpen := false;
+
+ }
+
+}
+
+class WriterStream {
+ var footprint:set<object>;
+ var stream:seq<int>;
+ var isOpen:bool;
+
+ function Valid():bool
+ reads this, footprint;
+ {
+ !(null in footprint) && this in footprint && isOpen
+ }
+
+method Create() //writing
+ modifies this;
+ ensures Valid() && fresh(footprint -{this});
+ ensures stream == [];
+ {
+ stream := [];
+ footprint := {this};
+ isOpen:= true;
+ }
+ method GetCount() returns (c:int)
+ requires Valid();
+ ensures 0<=c;
+ {
+ c:=|stream|;
+ }
+
+ method PutWord(w:Word )
+ requires Valid();
+ requires w != null;
+ modifies footprint;
+ ensures Valid() && fresh(footprint - old(footprint));
+ ensures old(stream)<= stream;
+ {
+ }
+ method PutWordInsideTag(tag:Word,w:Word )
+ requires Valid();
+ requires tag != null && w != null;
+ modifies footprint;
+ ensures Valid() && fresh(footprint - old(footprint));
+ ensures old(stream)<= stream;
+ {
+ }
+
+ method PutWordInsideHyperlink(tag:Word,w:Word )
+ requires Valid();
+ requires tag != null && w != null;
+ modifies footprint;
+ ensures Valid() && fresh(footprint - old(footprint));
+ ensures old(stream)<= stream;
+ {
+ }
+
+ method Close()
+ requires Valid();
+ modifies footprint;
+ {
+ isOpen := false;
+
+ }
+
+}
+
+
+
+
+class Map<Key,Value> {
+ var keys: seq<Key>;
+ var values: seq<Value>;
+
+
+ function Valid(): bool
+ reads this;
+ {
+ |keys| == |values| &&
+ (forall i, j :: 0 <= i && i < j && j < |keys| ==> keys[i] != keys[j])
+ }
+
+ method Init()
+ modifies this;
+ ensures Valid() && |keys| == 0;
+ {
+ keys := [];
+ values := [];
+ }
+
+ method Find(key: Key) returns (present: bool, val: Value)
+ requires Valid();
+ ensures !present ==> !(key in keys);
+ ensures present ==> (exists i :: 0 <= i && i < |keys| &&
+ keys[i] == key && values[i] == val);
+ {
+ var j;
+ call j := FindIndex(key);
+ if (j == -1) {
+ present := false;
+ } else {
+ present := true;
+ val := values[j];
+ }
+ }
+
+ method Add(key: Key, val: Value)
+ requires Valid();
+ modifies this;
+ ensures Valid();
+ // no key is lost:
+ ensures (forall k :: k in old(keys) ==> k in keys);
+ // at most one key is introduced:
+ ensures (forall k :: k in keys ==> k in old(keys) || k == key);
+ // the given key has the given value:
+ ensures (exists i :: 0 <= i && i < |keys| &&
+ keys[i] == key && values[i] == val);
+ // other values don't change:
+ ensures (forall i :: 0 <= i && i < |keys| && keys[i] != key ==>
+ values[i] == old(values)[i]);
+ {
+ var j;
+ call j := FindIndex(key);
+ if (j == -1) {
+ keys := keys + [key];
+ values := values + [val];
+ assert values[|keys|-1] == val; // lemma
+ } else {
+ keys := keys[..j] + [key] + keys[j+1..];
+ values := values[..j] + [val] + values[j+1..];
+ assert values[j] == val; //lemma
+ }
+ }
+
+ method Remove(key: Key)
+ requires Valid();
+ modifies this;
+ ensures Valid();
+ // no key is introduced:
+ ensures (forall k :: k in keys ==> k in old(keys));
+ // at most one key is removed:
+ ensures (forall k :: k in old(keys) ==> k in keys || k == key);
+ // the given key is not there:
+ // other values don't change:
+ ensures !(key in old(keys)) ==> keys == old(keys) && values == old(values);
+ ensures key in old(keys) ==>
+ !(key in keys) &&
+ (exists h ::
+ 0 <= h && h <= |keys| &&
+ keys[..h] == old(keys)[..h] &&
+ values[..h] == old(values)[..h] &&
+ keys[h..] == old(keys)[h+1..] &&
+ values[h..] == old(values)[h+1..]);
+ {
+ var j;
+ call j := FindIndex(key);
+ if (0 <= j) {
+ keys := keys[..j] + keys[j+1..];
+ values := values[..j] + values[j+1..];
+ }
+ }
+
+ method FindIndex(key: Key) returns (idx: int)
+ requires Valid();
+ ensures -1 <= idx && idx < |keys|;
+ ensures idx == -1 ==> !(key in keys);
+ ensures 0 <= idx ==> keys[idx] == key;
+ {
+ var j := 0;
+ while (j < |keys|)
+ invariant j <= |keys|;
+ invariant !(key in keys[..j]);
+ decreases |keys| -j;
+ {
+ if (keys[j] == key) {
+ idx := j;
+ return;
+ }
+ j := j + 1;
+ }
+ idx := -1;
+ }
+}
diff --git a/Test/VSI-Benchmarks/runtest.bat b/Test/VSI-Benchmarks/runtest.bat new file mode 100644 index 00000000..a8658aef --- /dev/null +++ b/Test/VSI-Benchmarks/runtest.bat @@ -0,0 +1,14 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+
+
+for %%f in ( b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% %* %%f
+)
|