Enhanced the VSI-Benchmarks tests:

- replaced the sequences used to specify permutations with multisets
- used some of the newer syntax in Dafny

5 files changed, 51 insertions, 89 deletions

diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy
index 3046621b..a7f1ca9a 100644
--- a/Test/VSI-Benchmarks/b2.dfy
+++ b/Test/VSI-Benchmarks/b2.dfy
@@ -2,18 +2,18 @@
 class Benchmark2 {

   method BinarySearch(a: array<int>, key: int) returns (result: int)

     requires a != null;

-    requires (forall i, j :: 0 <= i && i < j && j < a.Length ==> a[i] <= a[j]);

-    ensures -1 <= result && result < a.Length;

+    requires forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j];

+    ensures -1 <= result < a.Length;

     ensures 0 <= result ==> a[result] == key;

-    ensures result == -1 ==> (forall i :: 0 <= i && i < a.Length ==> a[i] != key);

+    ensures result == -1 ==> forall i :: 0 <= i < a.Length ==> a[i] != key;

   {

     var low := 0;

     var high := a.Length;

 

     while (low < high)

-      invariant 0 <= low && low <= high && high <= a.Length;

-      invariant (forall i :: 0 <= i && i < low ==> a[i] < key);

-      invariant (forall i :: high <= i && i < a.Length ==> key < a[i]);

+      invariant 0 <= low <= high <= a.Length;

+      invariant forall i :: 0 <= i < low ==> a[i] < key;

+      invariant forall i :: high <= i < a.Length ==> key < a[i];

     {

       var mid := low + (high - low) / 2;

       var midVal := a[mid];

@@ -49,7 +49,7 @@ method Main() {
 

 method TestSearch(a: array<int>, key: int)

   requires a != null;

-  requires (forall i, j :: 0 <= i && i < j && j < a.Length ==> a[i] <= a[j]);

+  requires forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j];

 {

   var b := new Benchmark2;

   var r := b.BinarySearch(a, key);

diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index 7cf3de07..9fc8a10d 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -27,7 +27,7 @@ class Queue<T> {
     reads this;

   { contents[0] }

   function method Get(i: int): T

-    requires 0 <= i && i < |contents|;

+    requires 0 <= i < |contents|;

     reads this;

   { contents[i] }

 }

@@ -40,58 +40,30 @@ 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>)

     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 :: 0 <= i && i < |perm|==> 0 <= perm[i] && perm[i] < |perm| );

-    ensures (forall i, j :: 0 <= i && i < j && j < |perm| ==> perm[i] != perm[j]); 

+    ensures forall i, j :: 0 <= i < j < |r.contents| ==> r.Get(i) <= r.Get(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]]);

+    ensures multiset(r.contents) == multiset(old(q.contents));

   {

     r := new Queue<int>.Init();

-    ghost var p := [];

-    

-    var n := 0;

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

-      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 :: 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]);

+      invariant |r.contents| + |q.contents| == |old(q.contents)|;

+      invariant forall i, j :: 0 <= i < j < |r.contents| ==> r.contents[i] <= r.contents[j];

+      invariant forall i, j ::

+                    0 <= i < |r.contents| &&

+                    0 <= j < |q.contents|

+                    ==> r.contents[i] <= q.contents[j];

       // the current array is that permutation of the input array

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

-    {  

+      invariant multiset(r.contents + q.contents) == multiset(old(q.contents));

+    {

+      ghost var qc := q.contents;

       var 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  

+      assert qc == qc[..k] + [m] + qc[k+1..];

       r.Enqueue(m);

-      pperm := pperm[k+1..|p|+1] + pperm[..k] + pperm[|p|+1..] + [pperm[k]];

     }

   }

   

@@ -100,8 +72,8 @@ class Benchmark3 {
     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 0 <= k < |old(q.contents)| && old(q.contents[k]) == m;

+    ensures forall i :: 0 <= i < |q.contents| ==> m <= q.contents[i];

     ensures q.contents == old(q.contents)[k+1..] + old(q.contents)[..k];  

   {

     var n := |q.contents|;

@@ -112,8 +84,8 @@ class Benchmark3 {
     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 0 <= k < |old(q.contents)| && old(q.contents)[k] == m;

+      invariant forall i :: 0 <= i < j ==> m <= old(q.contents)[i]; //m is min so far

     {

       var x := q.Dequeue();

       q.Enqueue(x);

diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy
index d5a56df4..6830fd87 100644
--- a/Test/VSI-Benchmarks/b4.dfy
+++ b/Test/VSI-Benchmarks/b4.dfy
@@ -27,7 +27,7 @@ class Map<Key(==),Value> {
     this in Repr &&

     |Keys| == |Values| && |nodes| == |Keys| + 1 &&

     head == nodes[0] &&

-    (forall i :: 0 <= i && i < |Keys| ==>

+    (forall i :: 0 <= i < |Keys| ==>

         nodes[i] != null &&

         nodes[i] in Repr &&

         nodes[i].key == Keys[i] && nodes[i].key !in Keys[i+1..] &&

@@ -51,7 +51,7 @@ class Map<Key(==),Value> {
   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 ==> exists i :: 0 <= i < |Keys| && Keys[i] == key && Values[i] == val;

   {

     var p, n, prev := FindIndex(key);

     if (p == null) {

@@ -66,11 +66,11 @@ class Map<Key(==),Value> {
     requires Valid();

     modifies Repr;

     ensures Valid() && fresh(Repr - old(Repr));

-    ensures (forall i :: 0 <= i && i < |old(Keys)| && old(Keys)[i] == key ==>

+    ensures forall i :: 0 <= 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]));

+                (forall j :: 0 <= 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);

   {

     var p, n, prev := FindIndex(key);

@@ -100,7 +100,7 @@ class Map<Key(==),Value> {
     ensures key in old(Keys) ==>

             |Keys| == |old(Keys)| - 1 && key !in Keys &&

             (exists h ::

-              0 <= h && h < |old(Keys)| &&

+              0 <= h < |old(Keys)| &&

               Keys[..h] == old(Keys)[..h] &&

               Values[..h] == old(Values)[..h] &&

               Keys[h..] == old(Keys)[h+1..] &&

diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy
index d6759c5f..8d218ec9 100644
--- a/Test/VSI-Benchmarks/b7.dfy
+++ b/Test/VSI-Benchmarks/b7.dfy
@@ -23,7 +23,7 @@ class Queue<T> {
     reads this;

   { contents[0] }

   function Get(i: int): T

-    requires 0 <= i && i < |contents|;

+    requires 0 <= i < |contents|;

     reads this;

   { contents[i] }

 }

@@ -101,20 +101,14 @@ class Stream {
 

 

 class Client {

-  method Sort(q: Queue<int>) returns (r: Queue<int>, perm:seq<int>)

+  method Sort(q: Queue<int>) returns (r: Queue<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]); 

+    ensures forall i, j :: 0 <= i < j < |r.contents| ==> r.Get(i) <= r.Get(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 multiset(r.contents) == multiset(old(q.contents));

   

   method Main()

   {

@@ -136,8 +130,7 @@ class Client {
     }

       

     rd.Close();

-    var perm;

-    q,perm := Sort(q);

+    q := Sort(q);

       

     var wr := new Stream;

     wr.Create();

diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index 2149df25..7608ed85 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -21,14 +21,14 @@ class Queue<T> {
     reads this;

   { contents[0] }

   function Get(i: int): T

-    requires 0 <= i && i < |contents|;

+    requires 0 <= i < |contents|;

     reads this;

   { contents[i] }

 }

 

 

 class Glossary {

-  method Sort(q: Queue<Word>) returns (r: Queue<Word>, perm:seq<int>)

+  method Sort(q: Queue<Word>) returns (r: Queue<Word>)

     requires q != null;

     modifies q;

     ensures r != null && fresh(r);

@@ -36,12 +36,8 @@ class Glossary {
     ensures (forall i, j :: 0 <= i && i < j && j < |r.contents| ==>

                 r.Get(i) != null &&

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

+    ensures multiset(r.contents) == multiset(old(q.contents));

 

   method Main()

   {

@@ -70,20 +66,21 @@ class Glossary {
         q.Enqueue(term);

       }

     }    

-    

+

     rs.Close();

-    var p;

-    q,p := Sort(q);

+    ghost var qc := q.contents;

+    q := Sort(q);

+    assert forall k :: k in q.contents ==> k in multiset(q.contents);

     var wr := new WriterStream;

     wr.Create();

-    

+

     while (0 < |q.contents|)

       invariant wr.Valid() && fresh(wr.footprint);

       invariant glossary.Valid();

       invariant glossary !in wr.footprint && null !in glossary.keys;

-      invariant (forall d :: d in glossary.values ==> null !in d);

+      invariant forall d :: d in glossary.values ==> null !in d;

       invariant q !in wr.footprint;

-      invariant (forall k :: k in q.contents ==> k in glossary.keys);

+      invariant forall k :: k in q.contents ==> k in glossary.keys;

     {

       var term := q.Dequeue();

       var present,definition := glossary.Find(term);

@@ -258,7 +255,7 @@ class Map<Key(==),Value> {
     reads this;

   {

     |keys| == |values| &&

-    (forall i, j :: 0 <= i && i < j && j < |keys| ==> keys[i] != keys[j])

+    (forall i, j :: 0 <= i < j < |keys| ==> keys[i] != keys[j])

   }

 

   method Init()

@@ -272,7 +269,7 @@ class Map<Key(==),Value> {
   method Find(key: Key) returns (present: bool, val: Value)

     requires Valid();

     ensures !present ==> key !in keys;

-    ensures present ==> (exists i :: 0 <= i && i < |keys| &&

+    ensures present ==> (exists i :: 0 <= i < |keys| &&

                                      keys[i] == key && values[i] == val);

   {

     var j := FindIndex(key);

@@ -288,10 +285,10 @@ class Map<Key(==),Value> {
     requires Valid();

     modifies this;

     ensures Valid();

-    ensures (forall i :: 0 <= i && i < |old(keys)| && old(keys)[i] == key ==>

+    ensures (forall i :: 0 <= 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]));

+              (forall j :: 0 <= 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];

   {

     var j := FindIndex(key);

@@ -317,7 +314,7 @@ class Map<Key(==),Value> {
     ensures key in old(keys) ==>

             |keys| == |old(keys)| - 1 && key !in keys &&

             (exists h ::

-              0 <= h && h <= |keys| &&

+              0 <= h <= |keys| &&

               keys[..h] == old(keys)[..h] &&

               values[..h] == old(values)[..h] &&

               keys[h..] == old(keys)[h+1..] &&