diff options
| -rw-r--r-- | Test/VSI-Benchmarks/b3.dfy | 84 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b4.dfy | 166 |
2 files changed, 147 insertions, 103 deletions
diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy index d9acfe04..19f54d94 100644 --- a/Test/VSI-Benchmarks/b3.dfy +++ b/Test/VSI-Benchmarks/b3.dfy @@ -40,8 +40,7 @@ class Comparable { class Benchmark3 {
-
- method Sort(q: Queue<int>) returns (r: Queue<int>, ghost perm:seq<int>)
+ method Sort(q: Queue<int>) returns (r: Queue<int>, ghost perm: seq<int>)
requires q != null;
modifies q;
ensures r != null && fresh(r);
@@ -49,27 +48,27 @@ class Benchmark3 { 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]]);
+ ensures |perm| == |r.contents|; // ==|pperm|
+ ensures (forall i :: 0 <= i && i < |perm|==> 0 <= perm[i] && perm[i] < |perm| );
+ ensures (forall i, j :: 0 <= i && i < j && j < |perm| ==> perm[i] != perm[j]);
+ // the final Queue is a permutation of the input Queue
+ ensures (forall i :: 0 <= i && i < |perm| ==> r.contents[i] == old(q.contents)[perm[i]]);
{
r := new Queue<int>;
call r.Init();
- ghost var p:= [];
+ ghost var p := [];
var n := 0;
- while (n < |q.contents|)
- invariant n <= |q.contents|;
- invariant n == |p|;
- invariant (forall i: int :: 0 <= i && i < n ==> p[i] == i);
- {
- p := p + [n];
- n := n + 1;
- }
- perm:= [];
- ghost var pperm := p + perm;
+ while (n < |q.contents|)
+ invariant n <= |q.contents|;
+ invariant n == |p|;
+ invariant (forall i :: 0 <= i && i < n ==> p[i] == i);
+ {
+ p := p + [n];
+ n := n + 1;
+ }
+ perm := [];
+ ghost var pperm := p + perm;
while (|q.contents| != 0)
invariant |r.contents| == |old(q.contents)| - |q.contents|;
@@ -81,26 +80,26 @@ class Benchmark3 { ==> 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]);
+ invariant pperm == p + perm && |p| == |q.contents| && |perm| == |r.contents|;
+ invariant (forall i :: 0 <= i && i < |perm| ==> 0 <= perm[i] && perm[i] < |pperm|);
+ invariant (forall i :: 0 <= i && i < |p| ==> 0 <= p[i] && p[i] < |pperm|);
+ invariant (forall i, j :: 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]]);
+ invariant (forall i :: 0 <= i && i < |perm| ==> r.contents[i] == old(q.contents)[perm[i]]);
+ invariant (forall i :: 0 <= i && i < |p| ==> q.contents[i] == old(q.contents)[p[i]]);
{
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
+ 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]];
+ 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]); //lemma needed to trigger axiom
- }
+ assert (forall i :: 0 <= i && i < |perm| ==> perm[i] == pperm[i]); //lemma 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
+ 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;
@@ -113,29 +112,28 @@ class Benchmark3 { m := q.Head();
var j := 0;
- while (j <n)
+ 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
+ invariant (forall i :: 0<= i && i < j ==> m <= old(q.contents)[i]); //m is min so far
{
- call x:= q.Dequeue();
- call q.Enqueue(x);
- if ( x < m) {k := j; m := x;}
- j:= j+1;
-
+ call x:= q.Dequeue();
+ call q.Enqueue(x);
+ if (x < m) { k := j; m := x; }
+ j := j+1;
}
- j := 0;
+ j := 0;
while (j < k)
invariant j <= k;
invariant q.contents == old(q.contents)[j..] + old(q.contents)[..j];
- {
+ {
call x := q.Dequeue();
call q.Enqueue(x);
- j:= j +1;
+ j := j+1;
}
-
- call m:= q.Dequeue();
- }
+
+ call m:= q.Dequeue();
+ }
}
diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy index d2fca9bc..fdb23379 100644 --- a/Test/VSI-Benchmarks/b4.dfy +++ b/Test/VSI-Benchmarks/b4.dfy @@ -1,107 +1,153 @@ // 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.
+// Note: The abstract specifications would do well with a map from keys
+// to values. However, Dafny does not support maps. Instead, such a
+// map is modeled by two sequences, one for the keys and one for the values.
+// The indices in these sequences correspond, so the dictionary maps
+// Keys[i] to Values[i].
+// The implementation uses a linked list, which isn't the most efficient
+// representation of a dictionary. However, for the benchmark, it shows
+// that the specification can use mathematical sequences while the
+// implementation uses a linked list.
class Map<Key,Value> {
- var keys: seq<Key>;
- var values: seq<Value>;
+ ghost var Keys: seq<Key>;
+ ghost var Values: seq<Value>;
+ ghost var Repr: set<object>;
+
+ var head: Node<Key,Value>;
+ ghost var nodes: seq<Node<Key,Value>>;
function Valid(): bool
- reads this;
+ reads this, Repr;
{
- |keys| == |values| &&
- (forall i, j :: 0 <= i && i < j && j < |keys| ==> keys[i] != keys[j])
+ this in Repr &&
+ |Keys| == |Values| && |nodes| == |Keys| + 1 &&
+ head == nodes[0] &&
+ (forall i :: 0 <= i && i < |Keys| ==>
+ nodes[i] != null &&
+ nodes[i] in Repr &&
+ nodes[i].key == Keys[i] && nodes[i].key !in Keys[i+1..] &&
+ nodes[i].val == Values[i] &&
+ nodes[i].next == nodes[i+1]) &&
+ nodes[|nodes|-1] == null
}
method Init()
modifies this;
- ensures Valid() && |keys| == 0;
+ ensures Valid() && fresh(Repr - {this});
+ ensures |Keys| == 0;
{
- keys := [];
- values := [];
+ Keys := [];
+ Values := [];
+ Repr := {this};
+ head := null;
+ nodes := [null];
}
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);
+ ensures !present ==> key !in Keys;
+ ensures present ==> (exists i :: 0 <= i && i < |Keys| && Keys[i] == key && Values[i] == val);
{
- call j := FindIndex(key);
- if (j == -1) {
+ call p, n, prev := FindIndex(key);
+ if (p == null) {
present := false;
} else {
+ val := p.val;
present := true;
- val := values[j];
}
}
method Add(key: Key, val: Value)
requires Valid();
- modifies this;
- ensures Valid();
- ensures (forall i :: 0 <= i && i < |old(keys)| && old(keys)[i] == key ==>
- |keys| == |old(keys)| &&
- keys[i] == key && values[i] == val &&
- (forall j :: 0 <= j && j < |values| && i != j ==> keys[j] == old(keys)[j] && values[j] == old(values)[j]));
- ensures key !in old(keys) ==> keys == old(keys) + [key] && values == old(values) + [val];
+ modifies Repr;
+ ensures Valid() && fresh(Repr - old(Repr));
+ ensures (forall i :: 0 <= i && i < |old(Keys)| && old(Keys)[i] == key ==>
+ |Keys| == |old(Keys)| &&
+ Keys[i] == key && Values[i] == val &&
+ (forall j :: 0 <= j && j < |Values| && i != j ==>
+ Keys[j] == old(Keys)[j] && Values[j] == old(Values)[j]));
+ ensures key !in old(Keys) ==> Keys == [key] + old(Keys) && Values == [val] + old(Values);
{
- call j := FindIndex(key);
- if (j == -1) {
- keys := keys + [key];
- values := values + [val];
+ call p, n, prev := FindIndex(key);
+ if (p == null) {
+ var h := new Node<Key,Value>;
+ h.key := key; h.val := val; h.next := head;
+ head := h;
+ Keys := [key] + Keys; Values := [val] + Values;
+ nodes := [h] + nodes;
+ Repr := Repr + {h};
} else {
- values := values[j := val];
+ p.val := val;
+ Values := Values[n := val];
}
}
method Remove(key: Key)
requires Valid();
- modifies this;
- ensures Valid();
+ modifies Repr;
+ ensures Valid() && fresh(Repr - old(Repr));
// no key is introduced:
- ensures (forall k :: k in keys ==> k in old(keys));
+ 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:
+ ensures (forall k :: k in old(Keys) ==> k in Keys || k == key);
// other values don't change:
- ensures key !in old(keys) ==> keys == old(keys) && values == old(values);
- ensures key in old(keys) ==>
- |keys| == |old(keys)| - 1 && key !in keys &&
+ ensures key !in old(Keys) ==> Keys == old(Keys) && Values == old(Values);
+ ensures key in old(Keys) ==>
+ |Keys| == |old(Keys)| - 1 && 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..]);
+ 0 <= h && h < |old(Keys)| &&
+ Keys[..h] == old(Keys)[..h] &&
+ Values[..h] == old(Values)[..h] &&
+ Keys[h..] == old(Keys)[h+1..] &&
+ Values[h..] == old(Values)[h+1..]);
{
- call j := FindIndex(key);
- if (0 <= j) {
- keys := keys[..j] + keys[j+1..];
- values := values[..j] + values[j+1..];
+ call p, n, prev := FindIndex(key);
+ if (p != null) {
+ Keys := Keys[..n] + Keys[n+1..];
+ assert Keys[..n] == old(Keys)[..n] && Keys[n..] == old(Keys)[n+1..];
+ Values := Values[..n] + Values[n+1..];
+ assert Values[..n] == old(Values)[..n] && Values[n..] == old(Values)[n+1..];
+ nodes := nodes[..n] + nodes[n+1..];
+ if (prev == null) {
+ head := head.next;
+ } else {
+ prev.next := p.next;
+ }
}
}
- method FindIndex(key: Key) returns (idx: int)
+ /*private*/ method FindIndex(key: Key) returns (p: Node<Key,Value>, ghost n: int, prev: Node<Key,Value>)
requires Valid();
- ensures -1 <= idx && idx < |keys|;
- ensures idx == -1 ==> key !in keys;
- ensures 0 <= idx ==> keys[idx] == key;
+ ensures p == null ==> key !in Keys;
+ ensures p != null ==>
+ 0 <= n && n < |Keys| && Keys[n] == key &&
+ key !in Keys[..n] && key !in Keys[n+1..] &&
+ p == nodes[n] &&
+ ((n == 0 && prev == null) || (0 < n && prev == nodes[n-1]));
{
- var j := 0;
- while (j < |keys|)
- invariant j <= |keys|;
- invariant key !in keys[..j];
+ n := 0;
+ prev := null;
+ p := head;
+ while (p != null)
+ invariant n <= |Keys| && p == nodes[n];
+ invariant key !in Keys[..n];
+ invariant (n == 0 && prev == null) || (0 < n && prev == nodes[n-1]);
+ decreases |Keys| - n;
{
- if (keys[j] == key) {
- idx := j;
+ if (p.key == key) {
return;
+ } else {
+ n := n + 1;
+ prev := p;
+ p := p.next;
}
- j := j + 1;
}
- idx := -1;
}
}
+
+class Node<Key,Value> {
+ var key: Key;
+ var val: Value;
+ var next: Node<Key,Value>;
+}
|