diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-03-15 14:44:20 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-03-15 14:44:20 -0700 |
| commit | f73c3a1f909f55bee986b654f05013df96d3ad7c (patch) | |
| tree | 8195349a4e1b0ebae8cc84fc22dca4e7e6405be3 /Test/dafny2 | |
| parent | c5da421a61b3c6a2089f54af053e92e3a72fc2eb (diff) | |
Dafny: added StoreAndRetrieve refinement example
Diffstat (limited to 'Test/dafny2')
| -rw-r--r-- | Test/dafny2/Answer | 4 | ||||
| -rw-r--r-- | Test/dafny2/StoreAndRetrieve.dfy | 72 | ||||
| -rw-r--r-- | Test/dafny2/runtest.bat | 1 |
3 files changed, 77 insertions, 0 deletions
diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer index ea481dae..381b9cb1 100644 --- a/Test/dafny2/Answer +++ b/Test/dafny2/Answer @@ -30,3 +30,7 @@ Dafny program verifier finished with 23 verified, 0 errors -------------------- Intervals.dfy --------------------
Dafny program verifier finished with 5 verified, 0 errors
+
+-------------------- StoreAndRetrieve.dfy --------------------
+
+Dafny program verifier finished with 22 verified, 0 errors
diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy new file mode 100644 index 00000000..1357b65c --- /dev/null +++ b/Test/dafny2/StoreAndRetrieve.dfy @@ -0,0 +1,72 @@ +module A imports Library {
+ class {:autocontracts} StoreAndRetrieve<Thing> {
+ ghost var Contents: set<Thing>;
+ predicate Valid
+ {
+ true
+ }
+ constructor Init()
+ {
+ Contents := {};
+ }
+ method Store(t: Thing)
+ {
+ Contents := Contents + {t};
+ }
+ method Retrieve(matchCriterion: Function) returns (thing: Thing)
+ requires exists t :: t in Contents && Function.Apply(matchCriterion, t);
+ ensures Contents == old(Contents);
+ ensures thing in Contents && Function.Apply(matchCriterion, thing);
+ {
+ var k; assume k in Contents && Function.Apply(matchCriterion, k);
+ thing := k;
+ }
+ }
+}
+
+module B refines A {
+ class StoreAndRetrieve<Thing> {
+ var arr: seq<Thing>;
+ predicate Valid
+ {
+ Contents == set x | x in arr
+ }
+ constructor Init()
+ {
+ arr := [];
+ }
+ method Store...
+ {
+ arr := arr + [t];
+ }
+ method Retrieve...
+ {
+ var i := 0;
+ while (i < |arr|)
+ invariant i < |arr|;
+ invariant forall j :: 0 <= j < i ==> !Function.Apply(matchCriterion, arr[j]);
+ {
+ if (Function.Apply(matchCriterion, arr[i])) { break; }
+ i := i + 1;
+ }
+ var k := arr[i]; assert ...;
+ }
+ }
+}
+
+module C refines B {
+ class StoreAndRetrieve<Thing> {
+ method Retrieve...
+ {
+ ...;
+ arr := [thing] + arr[..i] + arr[i+1..]; // LRU behavior
+ }
+ }
+}
+
+module Library {
+ // This class simulates function parameters
+ class Function {
+ static function method Apply<T>(f: Function, t: T): bool
+ }
+}
diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat index 79ee0f89..a4796939 100644 --- a/Test/dafny2/runtest.bat +++ b/Test/dafny2/runtest.bat @@ -15,6 +15,7 @@ for %%f in ( COST-verif-comp-2011-3-TwoDuplicates.dfy
COST-verif-comp-2011-4-FloydCycleDetect.dfy
Intervals.dfy
+ StoreAndRetrieve.dfy
) do (
echo.
echo -------------------- %%f --------------------
|