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).

1 files changed, 2 insertions, 2 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