digraph_reach.sil

// 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))
}