Enhanced the VSI-Benchmarks tests:

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

1 files changed, 18 insertions, 46 deletions

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