Dafny: removed allocated, changed semantics of fresh

-allocated(x) removed, as really only useful in old(...)
-old(allocated(x)) and !fresh(x) are equivalent (for x with type ref, set, sequence, and datatype).

2 files changed, 5 insertions, 4 deletions

diff --git a/Test/dafny1/SchorrWaite-stages.dfy b/Test/dafny1/SchorrWaite-stages.dfy
index 5a4da8ce..094e7be7 100644
--- a/Test/dafny1/SchorrWaite-stages.dfy
+++ b/Test/dafny1/SchorrWaite-stages.dfy
@@ -213,9 +213,9 @@ ghost module M2 refines M1 {
       // references, we need to make sure we can deal with the proof obligation for the path

       // argument.  For this reason, we add invariants that say that "path" and the .pathFromRoot

       // field of all marked nodes contain values that make sense in the pre-state.

-      invariant old(allocated(path)) && old(ReachableVia(root, path, t, S));

+      invariant !fresh(path) && old(ReachableVia(root, path, t, S));

       invariant forall n :: n in S && n.marked ==> var pth := n.pathFromRoot;

-                  old(allocated(pth)) && old(ReachableVia(root, pth, n, S));

+                  !fresh(pth) && old(ReachableVia(root, pth, n, S));

       invariant forall n :: n in S && n.marked ==> old(Reachable(root, n, S));

 

       decreases *;  // keep postponing termination checking

diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy
index 8da32b05..18adf491 100644
--- a/Test/dafny1/SchorrWaite.dfy
+++ b/Test/dafny1/SchorrWaite.dfy
@@ -12,6 +12,7 @@ class Node {
 

 datatype Path = Empty | Extend(Path, Node);

 

+

 class Main {

   method RecursiveMark(root: Node, ghost S: set<Node>)

     requires root in S;

@@ -213,9 +214,9 @@ class Main {
                   (forall j :: 0 <= j && j < |n.children| ==>

                     j == n.childrenVisited || n.children[j] == old(n.children[j])));

       // every marked node is reachable:

-      invariant old(allocated(path));  // needed to show 'path' worthy as argument to old(Reachable(...))

+      invariant !fresh(path);  // needed to show 'path' worthy as argument to old(Reachable(...))

       invariant old(ReachableVia(root, path, t, S));

-      invariant (forall n, pth :: n in S && n.marked && pth == n.pathFromRoot ==> old(allocated(pth)));

+      invariant (forall n, pth :: n in S && n.marked && pth == n.pathFromRoot ==> !fresh(pth));

       invariant (forall n, pth :: n in S && n.marked && pth == n.pathFromRoot ==>

                   old(ReachableVia(root, pth, n, S)));

       invariant (forall n :: n in S && n.marked ==> old(Reachable(root, n, S)));