diff options
| author |  rustanleino <unknown> | 2010-03-12 09:46:44 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-03-12 09:46:44 +0000 |
| commit | 0e6f265ca9a826dddd65b05ec21b97fcd549dccd (patch) | |
| tree | 47aa45f17a019261a9c3eec99b109d0cf3cefd6e /Test/dafny0/SchorrWaite.dfy | |
| parent | e0a48b3b117393f7926c5723eb789db4fdea3267 (diff) | |
Added wellformedness checks to method specifications
Diffstat (limited to 'Test/dafny0/SchorrWaite.dfy')
| -rw-r--r-- | Test/dafny0/SchorrWaite.dfy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/dafny0/SchorrWaite.dfy b/Test/dafny0/SchorrWaite.dfy index 527d379f..fb06d211 100644 --- a/Test/dafny0/SchorrWaite.dfy +++ b/Test/dafny0/SchorrWaite.dfy @@ -42,7 +42,7 @@ class Main { ensures (forall n :: n in S && n.marked ==>
n in stackNodes ||
(forall ch :: ch in n.children && ch != null ==> ch in S && ch.marked));
- ensures (forall n: Node :: old(n.marked) ==> n.marked);
+ ensures (forall n: Node :: n in S && old(n.marked) ==> n.marked);
ensures (forall n :: n in S ==>
n.childrenVisited == old(n.childrenVisited) &&
n.children == old(n.children));
@@ -58,7 +58,7 @@ class Main { (forall ch :: ch in n.children && ch != null ==> ch in S && ch.marked));
invariant (forall j :: 0 <= j && j < i ==>
root.children[j] == null || root.children[j].marked);
- invariant (forall n: Node :: old(n.marked) ==> n.marked);
+ invariant (forall n: Node :: n in S && old(n.marked) ==> n.marked);
invariant (forall n :: n in S ==>
n.childrenVisited == old(n.childrenVisited) &&
n.children == old(n.children));
|