From 07cc86c1de92e885393058a24e1cbbb9301c0715 Mon Sep 17 00:00:00 2001
From: Jason Koenig <unknown>
Date: Sun, 29 Jul 2012 13:29:41 -0700
Subject: 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).
---
 Test/dafny1/SchorrWaite-stages.dfy | 4 ++--
 Test/dafny1/SchorrWaite.dfy        | 5 +++--
 2 files changed, 5 insertions(+), 4 deletions(-)

(limited to 'Test/dafny1')

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