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

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>;

+}