From eea33dbb4caf784b3f49f4ebacda75c9f1ed394b Mon Sep 17 00:00:00 2001 From: rustanleino Date: Mon, 14 Jun 2010 22:51:06 +0000 Subject: Dafny: * changed implementation of Test/VSI-Benchmarks/b4.dfy to be more interesting (and, in particular, different from the specification) * reformatted Test/VSI-Benchmarks/b3.dfy --- Test/VSI-Benchmarks/b3.dfy | 84 +++++++++++------------ Test/VSI-Benchmarks/b4.dfy | 166 +++++++++++++++++++++++++++++---------------- 2 files changed, 147 insertions(+), 103 deletions(-) (limited to 'Test/VSI-Benchmarks') 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) returns (r: Queue, ghost perm:seq) + method Sort(q: Queue) returns (r: Queue, ghost perm: seq) 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; 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) returns (m: int, k:int) //m is the min, k is m's index in q + method RemoveMin(q: Queue) 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 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 { - var keys: seq; - var values: seq; + ghost var Keys: seq; + ghost var Values: seq; + ghost var Repr: set; + + var head: Node; + ghost var nodes: seq>; 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; + 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, ghost n: int, prev: Node) 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 { + var key: Key; + var val: Value; + var next: Node; +} -- cgit v1.2.3