Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- // class Node
- field left: Ref
- field right: Ref
- field is_marked: Bool
- predicate inv(node: Ref, graph: Set[Ref]) {
- node != null
- && acc(node.left)
- && acc(node.right)
- && acc(node.is_marked)
- && (node.left != null ==> acc(inv(node.left, graph)))
- && (node.right != null ==> acc(inv(node.right, graph)))
- && node in graph
- && (forall a: Ref :: a in graph ==> acc(a.left))
- && (forall b: Ref :: b in graph ==> acc(b.right))
- && (forall c: Ref :: c in graph ==> acc(c.is_marked))
- && (forall x: Ref :: x in graph ==> (x.left != null ==> x.left in graph))
- && (forall y: Ref :: y in graph ==> (y.right != null ==> y.right in graph))
- }
- method reach(graph: Set[Ref], node: Ref) returns (reached: Set[Ref])
- requires acc(inv(node, graph))
- ensures acc(inv(node, graph))
- //TODO: ensures acc(inv(node, reached))
- {
- unfold acc(inv(node, graph))
- var left_reached: Set[Ref] := Set[Ref]()
- if (node.left != null && !node.left.is_marked) {
- node.left.is_marked := true
- left_reached := reach(graph, node.left)
- }
- var right_reached: Set[Ref] := Set[Ref]()
- if (node.right != null && !node.right.is_marked) {
- node.right.is_marked := true
- right_reached := reach(graph, node.right)
- }
- reached := (left_reached) union Set(node) union (right_reached)
- fold acc(inv(node, graph))
- }
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement