Dafny: reinstated autocontracts

3 files changed, 14 insertions, 8 deletions

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 (