diff options
| -rw-r--r-- | Chalice/refinements/DSW.chalice | 61 |
1 files changed, 58 insertions, 3 deletions
diff --git a/Chalice/refinements/DSW.chalice b/Chalice/refinements/DSW.chalice index fc65b850..78a84354 100644 --- a/Chalice/refinements/DSW.chalice +++ b/Chalice/refinements/DSW.chalice @@ -5,6 +5,8 @@ class Node { var children: seq<Node>; var marked: bool; ghost var path: seq<Node>; + + var parent: Node; } class DSW0 { @@ -55,9 +57,13 @@ class DSW0 { invariant forall n in S :: n.children == old(n.children); // termination invariant stop ==> |stack| == 0 && (forall ch in t.children :: ch.marked); - { - var s:seq<Node> := t.children; - var n:Node [rd(s[*].marked), rd(s[*].marked) && n in t.children && ! n.marked]; + { + var n: Node; + + // stupid syntactic trick to make transformers go around call + if (true) { + call n := PickUnmarked(t.children); + } if (n != null) { // push @@ -77,6 +83,55 @@ class DSW0 { } } } + + method PickUnmarked(p: seq<Node>) returns (x: Node) + requires rd(p[*].marked); + requires forall n in p :: n != null; + ensures rd(p[*].marked); + ensures x != null ==> x in p && ! x.marked; + ensures x == null ==> (forall n in p :: n.marked); + { + var x [(exists n in p :: !n.marked) ? (x in p && !x.marked) : (x == null)] + } } +class DSW1 refines DSW0 { + transforms IterativeMark(root: Node, S: seq<Node>) + { + assume forall n in S :: n.parent == null; + _ + while + invariant forall n in S :: n !in stack ==> n.parent == null; + invariant forall i in [1..|stack|] :: stack[i-1].parent == stack[i]; + { + _ + if {*} + if { + // push + if (|stack| > 0) { + t.parent := stack[0]; + } + * + } else { + // pop + if {*} else { + _ + t.parent := null; + } + } + } + } + transforms PickUnmarked(p: seq<Node>) returns (x: Node) + { + replaces x by { + if (|p| == 0) { + x := null; + } else if (! p[0].marked) { + x := p[0]; + } else { + call x := PickUnmarked(p[1..]); + } + } + } +}
\ No newline at end of file |