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, 3 insertions, 2 deletions

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