Dafny:

* Added arrays
* Beefed up set axiomatization to know more things about set displays
* Added a simple heuristic that can infer some simple decreases clauses for loops
* Added Dafny solutions to a couple of VACID benchmarks

6 files changed, 19 insertions, 64 deletions

diff --git a/Test/VSI-Benchmarks/Answer b/Test/VSI-Benchmarks/Answer
index 1efeba04..2a4587f4 100644
--- a/Test/VSI-Benchmarks/Answer
+++ b/Test/VSI-Benchmarks/Answer
@@ -5,7 +5,7 @@ Dafny program verifier finished with 10 verified, 0 errors
 

 -------------------- b2.dfy --------------------

 

-Dafny program verifier finished with 12 verified, 0 errors

+Dafny program verifier finished with 6 verified, 0 errors

 

 -------------------- b3.dfy --------------------

 

diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy
index ec255ed1..fd20a72b 100644
--- a/Test/VSI-Benchmarks/b2.dfy
+++ b/Test/VSI-Benchmarks/b2.dfy
@@ -1,27 +1,23 @@
 

-// Note:Implemented arrays as Dafny does not provide them

-

 class Benchmark2 {

-  method BinarySearch(a: Array, key: int) returns (result: int)

+  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.Get(i) <= a.Get(j));

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

-    ensures 0 <= result ==> a.Get(result) == key;

-    ensures result == -1 ==>

-              (forall i :: 0 <= i && i < a.Length() ==> a.Get(i) != key);

+    requires (forall i, j :: 0 <= i && i < j && j < |a| ==> a[i] <= a[j]);

+    ensures -1 <= result && result < |a|;

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

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

   {

     var low := 0;

-    var high := a.Length();

+    var high := |a|;

 

     while (low < high)

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

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

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

+      invariant 0 <= low && low <= high && high <= |a|;

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

+      invariant (forall i :: high <= i && i < |a| ==> key < a[i]);

       decreases high - low;

     {

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

-      var midVal := a.Get(mid);

+      var midVal := a[mid];

 

       if (midVal < key) {

         low := mid + 1;

@@ -36,47 +32,13 @@ class Benchmark2 {
   }

 }

 

-class Array {

-  var contents: seq<int>;

-  method Init(n: int)

-    requires 0 <= n;

-    modifies this;

-    ensures |contents| == n;

-  {

-    var i := 0;

-    contents := [];

-    while (i < n)

-      invariant i <= n && i == |contents|;

-      decreases n - i;

-    {

-      contents := contents + [0];

-      i := i + 1;

-    }

-  }

-   function method Length(): int

-    reads this;

-  { |contents| }

-   function method Get(i: int): int

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

-    reads this;

-  { contents[i] }

-  method Set(i: int, x: int)

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

-    modifies this;

-    ensures contents == old(contents)[i := x];

-  {

-    contents := contents[i := x];

-  }

-}

-

 method Main() {

-  var a := new Array;

-  call a.Init(5);

-  call a.Set(0, -4);

-  call a.Set(1, -2);

-  call a.Set(2, -2);

-  call a.Set(3, 0);

-  call a.Set(4, 25);

+  var a := new int[5];

+  a[0] := -4;

+  a[1] := -2;

+  a[2] := -2;

+  a[3] := 0;

+  a[4] := 25;

   call TestSearch(a, 4);

   call TestSearch(a, -8);

   call TestSearch(a, -2);

@@ -86,9 +48,9 @@ method Main() {
   call TestSearch(a, 27);

 }

 

-method TestSearch(a: Array, key: int)

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

   requires a != null;

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

+  requires (forall i, j :: 0 <= i && i < j && j < |a| ==> a[i] <= a[j]);

 {

   var b := new Benchmark2;

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

diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index 37b73cba..6d9c3ddd 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -64,7 +64,6 @@ class Benchmark3 {
 		invariant n <= |q.contents|;

 		invariant n == |p|;

 		invariant (forall i: int :: 0 <= i && i < n ==> p[i] == i);

-		decreases |q.contents| - n;

    {

 		p := p + [n];

 		n := n + 1;

@@ -121,7 +120,6 @@ class Benchmark3 {
       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   

-      decreases n-j;

     {

 		call x:= q.Dequeue();

 		call q.Enqueue(x);

@@ -134,7 +132,6 @@ class Benchmark3 {
     while (j < k)

       invariant j <= k;

       invariant q.contents == old(q.contents)[j..] + old(q.contents)[..j]; 

-      decreases k-j;

     {     

       call x := q.Dequeue();

       call q.Enqueue(x);

diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy
index ab1285f6..d2fca9bc 100644
--- a/Test/VSI-Benchmarks/b4.dfy
+++ b/Test/VSI-Benchmarks/b4.dfy
@@ -95,7 +95,6 @@ class Map<Key,Value> {
     while (j < |keys|)

       invariant j <= |keys|;

       invariant key !in keys[..j];

-      decreases |keys| -j;

     {

       if (keys[j] == key) {

         idx := j;

diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy
index e5af6357..2304e602 100644
--- a/Test/VSI-Benchmarks/b7.dfy
+++ b/Test/VSI-Benchmarks/b7.dfy
@@ -142,7 +142,6 @@ class Client {
     call wr.Create();

     while (0 < |q.contents|)

       invariant wr.Valid() && fresh(wr.footprint) && fresh(q) && q !in wr.footprint;

-      decreases |q.contents|;

     {

       call ch := q.Dequeue();  

       call wr.PutChar(ch);    

diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index d8ee2013..34e0cfef 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -104,7 +104,6 @@ class Glossary {
         invariant q !in wr.footprint;

         invariant qcon == q.contents;

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

-        decreases |definition| -i;

       {

         var w := definition[i];

         call present, d := glossary.Find(w);

@@ -342,7 +341,6 @@ class Map<Key,Value> {
     while (j < |keys|)

       invariant j <= |keys|;

       invariant key !in keys[..j];

-      decreases |keys| -j;

     {

       if (keys[j] == key) {

         idx := j;