diff options
author | Jason Koenig <unknown> | 2012-07-02 11:51:44 -0700 |
---|---|---|
committer | Jason Koenig <unknown> | 2012-07-02 11:51:44 -0700 |
commit | 9e7a1c3d7cc7d4f077a36593eedce6f7a5accf22 (patch) | |
tree | b4fe6505a6e4584b80b81d14db6a1b557b580f8e /Test/dafny2/StoreAndRetrieve.dfy | |
parent | 44c908246d375995e0885cef212490e75bbcd96d (diff) |
Dafny: reinstated autocontracts
Diffstat (limited to 'Test/dafny2/StoreAndRetrieve.dfy')
-rw-r--r-- | Test/dafny2/StoreAndRetrieve.dfy | 15 |
1 files changed, 8 insertions, 7 deletions
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];
|