diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-10-22 01:30:55 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-10-22 01:30:55 -0700 |
| commit | aba7928452a9043ab1cc6f4fd2e0dda4e2273508 (patch) | |
| tree | 501b905b63f7e369112dfd702d915cbfe067893c /Test | |
| parent | 066cd4f2a054dd9acfa917ab0d89eed7d9b36d92 (diff) | |
allow a refinement to introduce "return" statements, at the price of re-verifying the postcondition at that time
let refined classes inherit attributes
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny3/Answer | 4 | ||||
| -rw-r--r-- | Test/dafny3/CachedContainer.dfy | 138 | ||||
| -rw-r--r-- | Test/dafny3/runtest.bat | 2 |
4 files changed, 144 insertions, 2 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 1725be19..fe9527f8 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1824,7 +1824,7 @@ Verifying CheckWellformed$$_1_M1.C.M ... [0 proof obligations] verified
Verifying Impl$$_1_M1.C.M ...
- [0 proof obligations] verified
+ [1 proof obligation] verified
Verifying CheckWellformed$$_1_M1.C.P ...
Superposition.dfy(47,15): Error BP5003: A postcondition might not hold on this return path.
diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer index 240883dd..5ab835e7 100644 --- a/Test/dafny3/Answer +++ b/Test/dafny3/Answer @@ -10,3 +10,7 @@ Dafny program verifier finished with 38 verified, 0 errors -------------------- Dijkstra.dfy --------------------
Dafny program verifier finished with 11 verified, 0 errors
+
+-------------------- CachedContainer.dfy --------------------
+
+Dafny program verifier finished with 47 verified, 0 errors
diff --git a/Test/dafny3/CachedContainer.dfy b/Test/dafny3/CachedContainer.dfy new file mode 100644 index 00000000..9bde80da --- /dev/null +++ b/Test/dafny3/CachedContainer.dfy @@ -0,0 +1,138 @@ +// give the method signatures and specs
+ghost module M0 {
+ class {:autocontracts} Container<T(==)> {
+ ghost var Contents: set<T>;
+ predicate Valid()
+ constructor ()
+ ensures Contents == {};
+ method Add(t: T)
+ ensures Contents == old(Contents) + {t};
+ method Remove(t: T)
+ ensures Contents == old(Contents) - {t};
+ method Contains(t: T) returns (b: bool)
+ ensures Contents == old(Contents);
+ ensures b <==> t in Contents;
+ }
+}
+
+// provide bodies for the methods
+ghost module M1 refines M0 {
+ class Container<T(==)> {
+ constructor... {
+ Contents := {};
+ }
+ method Add... {
+ Contents := Contents + {t};
+ }
+ method Remove... {
+ Contents := Contents - {t};
+ }
+ method Contains... {
+ // b := t in Contents;
+ b :| assume b <==> t in Contents;
+ }
+ }
+}
+
+// implement the set in terms of a sequence
+module M2 refines M1 {
+ class Container<T(==)> {
+ var elems: seq<T>;
+ predicate Valid()
+ {
+ Contents == (set x | x in elems) &&
+ forall i,j :: 0 <= i < j < |elems| ==> elems[i] != elems[j]
+ }
+ method FindIndex(t: T) returns (j: nat)
+ ensures j <= |elems|;
+ ensures if j < |elems| then elems[j] == t else t !in elems;
+ {
+ j := 0;
+ while (j < |elems|)
+ invariant j <= |elems|;
+ invariant forall i :: 0 <= i < j ==> elems[i] != t;
+ {
+ if (elems[j] == t) {
+ return;
+ }
+ j := j + 1;
+ }
+ }
+
+ constructor... {
+ elems := [];
+ }
+ method Add... {
+ var j := FindIndex(t);
+ if (j == |elems|) {
+ elems := elems + [t];
+ }
+ }
+ method Remove... {
+ var j := FindIndex(t);
+ if (j < |elems|) {
+ elems := elems[..j] + elems[j+1..];
+ }
+ }
+ method Contains... {
+ var j := FindIndex(t);
+ b := j < |elems|;
+ }
+ }
+}
+
+// implement a cache
+module M3 refines M2 {
+ class Container<T(==)> {
+ var cachedValue: T;
+ var cachedIndex: int;
+ predicate Valid() {
+ 0 <= cachedIndex ==> cachedIndex < |elems| && elems[cachedIndex] == cachedValue
+ }
+ constructor... {
+ cachedIndex := -1;
+ }
+ method FindIndex... {
+ if (0 <= cachedIndex && cachedValue == t) {
+ return cachedIndex;
+ }
+ }
+ method Remove... {
+ ...;
+ if ... {
+ if (cachedIndex == j) {
+ // clear the cache
+ cachedIndex := -1;
+ } else if (j < cachedIndex) {
+ // adjust for the shifting down
+ cachedIndex := cachedIndex - 1;
+ }
+ }
+ }
+ }
+}
+
+// here a client of the Container
+module Client {
+ import M as M0 default M2;
+ method Test() {
+ var c := new M.Container();
+ c.Add(56);
+ c.Add(12);
+ var b := c.Contains(17);
+ assert !b;
+ b := c.Contains(12);
+ assert b;
+ c.Remove(12);
+ b := c.Contains(12);
+ assert !b;
+ assert c.Contents == {56};
+ }
+}
+
+module CachedClient refines Client {
+ import M = M3;
+ method Main() {
+ Test();
+ }
+}
diff --git a/Test/dafny3/runtest.bat b/Test/dafny3/runtest.bat index f995daff..2ebba74a 100644 --- a/Test/dafny3/runtest.bat +++ b/Test/dafny3/runtest.bat @@ -4,7 +4,7 @@ setlocal set BINARIES=..\..\Binaries
set DAFNY_EXE=%BINARIES%\Dafny.exe
-for %%f in (Iter.dfy Streams.dfy Dijkstra.dfy) do (
+for %%f in (Iter.dfy Streams.dfy Dijkstra.dfy CachedContainer.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f
|