Dafny:

* Recoded frame axioms to be more goal directed
* Added Main test driver to Test/VSI-Benchmarks/b2.dfy

2 files changed, 2 insertions, 7 deletions

diff --git a/Test/VSI-Benchmarks/Answer b/Test/VSI-Benchmarks/Answer
index 926a4da3..1efeba04 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 8 verified, 0 errors

+Dafny program verifier finished with 12 verified, 0 errors

 

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

 

diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy
index 0cae993a..86c12854 100644
--- a/Test/VSI-Benchmarks/b2.dfy
+++ b/Test/VSI-Benchmarks/b2.dfy
@@ -63,16 +63,12 @@ class Array {
   method Set(i: int, x: int)

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

     modifies this;

-    ensures |contents| == |old(contents)|;

-    ensures contents[..i] == old(contents[..i]);

-    ensures contents[i] == x;

-    ensures contents[i+1..] == old(contents[i+1..]);

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

   {

     contents := contents[i := x];

   }

 }

 

-/******

 method Main() {

   var a := new Array;

   call a.Init(5);

@@ -103,4 +99,3 @@ method TestSearch(a: Array, key: int)
   call r := b.BinarySearch(a, key);

   print "Looking for key=", key, ", result=", r, "\n";

 }

-******/