Dafny: reinstated autocontracts

7 files changed, 24 insertions, 11 deletions

diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index b2876948..06cac03b 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -11,6 +11,10 @@ Dafny program verifier finished with 24 verified, 0 errors
 

 Dafny program verifier finished with 11 verified, 0 errors

 

+-------------------- ExtensibleArrayAuto.dfy --------------------

+

+Dafny program verifier finished with 11 verified, 0 errors

+

 -------------------- BinaryTree.dfy --------------------

 

 Dafny program verifier finished with 24 verified, 0 errors

diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat
index 22bef761..fa7f7c70 100644
--- a/Test/dafny1/runtest.bat
+++ b/Test/dafny1/runtest.bat
@@ -5,7 +5,7 @@ set BOOGIEDIR=..\..\Binaries
 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

 

 for %%f in (Queue.dfy PriorityQueue.dfy

-            ExtensibleArray.dfy

+            ExtensibleArray.dfy ExtensibleArrayAuto.dfy

             BinaryTree.dfy

             UnboundedStack.dfy

             SeparationLogicList.dfy

diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer
index f359e416..f466d813 100644
--- a/Test/dafny2/Answer
+++ b/Test/dafny2/Answer
@@ -27,6 +27,10 @@ Dafny program verifier finished with 4 verified, 0 errors
 

 Dafny program verifier finished with 23 verified, 0 errors

 

+-------------------- StoreAndRetrieve.dfy --------------------

+

+Dafny program verifier finished with 22 verified, 0 errors

+

 -------------------- Intervals.dfy --------------------

 

 Dafny program verifier finished with 5 verified, 0 errors

diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy
index 15c82d65..9ea7a3ff 100644
--- a/Test/dafny2/StoreAndRetrieve.dfy
+++ b/Test/dafny2/StoreAndRetrieve.dfy
@@ -1,4 +1,5 @@
-ghost module A imports Library {

+ghost module A {

+  module L = Library;

   class {:autocontracts} StoreAndRetrieve<Thing> {

     ghost var Contents: set<Thing>;

     predicate Valid

@@ -13,12 +14,12 @@ ghost module A imports Library {
     {

       Contents := Contents + {t};

     }

-    method Retrieve(matchCriterion: Function) returns (thing: Thing)

-      requires exists t :: t in Contents && Function.Apply(matchCriterion, t);

+    method Retrieve(matchCriterion: L.Function) returns (thing: Thing)

+      requires exists t :: t in Contents && L.Function.Apply(matchCriterion, t);

       ensures Contents == old(Contents);

-      ensures thing in Contents && Function.Apply(matchCriterion, thing);

+      ensures thing in Contents && L.Function.Apply(matchCriterion, thing);

     {

-      var k :| k in Contents && Function.Apply(matchCriterion, k);

+      var k :| k in Contents && L.Function.Apply(matchCriterion, k);

       thing := k;

     }

   }

@@ -44,9 +45,9 @@ module B refines A {
       var i := 0;

       while (i < |arr|)

         invariant i < |arr|;

-        invariant forall j :: 0 <= j < i ==> !Function.Apply(matchCriterion, arr[j]);

+        invariant forall j :: 0 <= j < i ==> !L.Function.Apply(matchCriterion, arr[j]);

       {

-        if (Function.Apply(matchCriterion, arr[i])) { break; }

+        if (L.Function.Apply(matchCriterion, arr[i])) { break; }

         i := i + 1;

       }

       var k := arr[i];

diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat
index 19b116d2..25dbed54 100644
--- a/Test/dafny2/runtest.bat
+++ b/Test/dafny2/runtest.bat
@@ -4,7 +4,7 @@ setlocal
 set BOOGIEDIR=..\..\Binaries

 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

 

-REM soon again:    SnapshotableTrees.dfy StoreAndRetrieve.dfy

+REM soon again:    SnapshotableTrees.dfy

 for %%f in (

     Classics.dfy

     TreeBarrier.dfy

@@ -13,6 +13,7 @@ for %%f in (
     COST-verif-comp-2011-2-MaxTree-datatype.dfy

     COST-verif-comp-2011-3-TwoDuplicates.dfy

     COST-verif-comp-2011-4-FloydCycleDetect.dfy

+    StoreAndRetrieve.dfy

     Intervals.dfy TreeFill.dfy TuringFactorial.dfy

     MajorityVote.dfy SegmentSum.dfy

   ) do (

diff --git a/Test/vstte2012/Answer b/Test/vstte2012/Answer
index 15a95de1..bca270c3 100644
--- a/Test/vstte2012/Answer
+++ b/Test/vstte2012/Answer
@@ -11,6 +11,10 @@ Dafny program verifier finished with 25 verified, 0 errors
 

 Dafny program verifier finished with 13 verified, 0 errors

 

+-------------------- RingBufferAuto.dfy --------------------

+

+Dafny program verifier finished with 13 verified, 0 errors

+

 -------------------- Tree.dfy --------------------

 

 Dafny program verifier finished with 15 verified, 0 errors

diff --git a/Test/vstte2012/runtest.bat b/Test/vstte2012/runtest.bat
index cda455fa..7f7c9b9f 100644
--- a/Test/vstte2012/runtest.bat
+++ b/Test/vstte2012/runtest.bat
@@ -4,11 +4,10 @@ setlocal
 set BOOGIEDIR=..\..\Binaries

 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

 

-REM removed for now: RingBufferAuto.dfy

 for %%f in (

     Two-Way-Sort.dfy

     Combinators.dfy

-    RingBuffer.dfy 

+    RingBuffer.dfy RingBufferAuto.dfy

     Tree.dfy

     BreadthFirstSearch.dfy

   ) do (