From aba7928452a9043ab1cc6f4fd2e0dda4e2273508 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Mon, 22 Oct 2012 01:30:55 -0700
Subject: allow a refinement to introduce "return" statements, at the price of
 re-verifying the postcondition at that time let refined classes inherit
 attributes

---
 Test/dafny3/Answer              |   4 ++
 Test/dafny3/CachedContainer.dfy | 138 ++++++++++++++++++++++++++++++++++++++++
 Test/dafny3/runtest.bat         |   2 +-
 3 files changed, 143 insertions(+), 1 deletion(-)
 create mode 100644 Test/dafny3/CachedContainer.dfy

(limited to 'Test/dafny3')

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