diff options
Diffstat (limited to 'Test/dafny1/SchorrWaite.dfy')
| -rw-r--r-- | Test/dafny1/SchorrWaite.dfy | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy index 52db9dca..0d69b1b8 100644 --- a/Test/dafny1/SchorrWaite.dfy +++ b/Test/dafny1/SchorrWaite.dfy @@ -211,7 +211,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 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 ==>
old(ReachableVia(root, pth, n, S)));
invariant (forall n :: n in S && n.marked ==> old(Reachable(root, n, S)));
|