From 9e7a1c3d7cc7d4f077a36593eedce6f7a5accf22 Mon Sep 17 00:00:00 2001
From: Jason Koenig <unknown>
Date: Mon, 2 Jul 2012 11:51:44 -0700
Subject: Dafny: reinstated autocontracts

---
 Test/dafny2/Answer               |  4 ++++
 Test/dafny2/StoreAndRetrieve.dfy | 15 ++++++++-------
 Test/dafny2/runtest.bat          |  3 ++-
 3 files changed, 14 insertions(+), 8 deletions(-)

(limited to 'Test/dafny2')

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 (
-- 
cgit v1.2.3