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 | dee846026331bfc0b97d11b98a69a5cd7cc6b06b (patch) | |
| tree | f3a287baabecb1ef940c1b556efe5a0c6caebf07 /Test/dafny2/StoreAndRetrieve.dfy | |
| parent | 99f724b08a690618252f256d99e61db132d291a3 (diff) | |
Dafny: added StoreAndRetrieve refinement example
Diffstat (limited to 'Test/dafny2/StoreAndRetrieve.dfy')
| -rw-r--r-- | Test/dafny2/StoreAndRetrieve.dfy | 72 |
1 files changed, 72 insertions, 0 deletions
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
+ }
+}
|