(* Depth-First Search
(following François Pottier's lecture INF431 at École Polytechnique)
We are given memory cells with two (possibly null) [left] and [right]
neighbours and a mutable Boolean attribute [marked]. In Java, it would
look like
class Cell { Cell left, right; boolean marked; ... }
We mark all cells that are reachable from a given cell [root] using
depth-first search, that is using the following recursive function:
static void dfs(Cell c) {
if (c != null && !c.marked) {
c.marked = true;
dfs(c.left);
dfs(c.right);
}
}
We wish to prove that, assuming that all cells are initially unmarked,
a call to dfs(root) will mark all cells reachable from root, and only
those cells.
*)
module DFS
use bool.Bool
use map.Map
use ref.Ref
type loc
val constant null: loc
val constant root: loc
val (==) (x y: loc) : bool
ensures { result <-> x = y }
val function left loc: loc
val function right loc: loc
type marks = map loc bool
val marked: ref marks
val ghost busy: ref marks
let set (m: ref marks) (l: loc) (b: bool) : unit
writes { m }
ensures { !m = (old !m)[l <- b] }
= let f = !m in
m := fun x -> if x == l then b else f x
predicate edge (x y: loc) = x <> null && (left x = y || right x = y)
inductive path (x y: loc) =
| path_nil: forall x: loc. path x x
| path_cons: forall x y z: loc. path x y -> edge y z -> path x z
predicate only_descendants_are_marked (marked: marks) =
forall x: loc. x <> null && marked[x] = True -> path root x
predicate well_colored (marked busy: marks) =
forall x y: loc. edge x y -> y <> null ->
busy[x] = True || (marked[x] = True -> marked[y] = True)
let rec dfs (c: loc) : unit
requires { well_colored !marked !busy }
requires { only_descendants_are_marked !marked }
requires { path root c }
diverges
ensures { well_colored !marked !busy }
ensures { forall x: loc. (old !marked)[x] = True -> !marked[x] = True }
ensures { c <> null -> !marked[c] = True }
ensures { forall x: loc. !busy[x] = True -> (old !busy)[x] = True }
ensures { only_descendants_are_marked !marked }
=
if not (c == null) && not !marked[c] then begin
ghost set busy c True;
set marked c True;
dfs (left c);
dfs (right c);
set busy c False
end
predicate all_descendants_are_marked (marked: marks) =
root <> null ->
marked[root] = True &&
forall x y: loc.
edge x y -> marked[x] = True -> y <> null -> marked[y] = True
lemma reformulation:
forall marked: marks.
all_descendants_are_marked marked ->
forall x: loc. x <> null -> path root x -> marked[x] = True /\ root <> null
let traverse () : unit
requires { forall x: loc. x <> null ->
!marked[x] = False && !busy[x] = False }
diverges
ensures { only_descendants_are_marked !marked }
ensures { all_descendants_are_marked !marked }
ensures { forall x: loc. x <> null -> !busy[x] = False }
=
assert { well_colored !marked !busy };
dfs root
end