## Depth-First Search

Marking reachable nodes in a graph with left and right pointers

**Authors:** Jean-Christophe Filliâtre

**Topics:** Graph Algorithms

**Tools:** Why3

see also the index (by topic, by tool, by reference, by year)

(* 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 import bool.Bool use import map.Map use import ref.Ref type loc constant null: loc constant root: loc function left loc: loc function right loc: loc type marks = map loc bool val marked: ref marks val ghost busy: ref marks 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 c <> null && not !marked[c] then begin ghost busy := !busy[c <- True]; marked := !marked[c <- True]; dfs (left c); dfs (right c); busy := !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

download ZIP archive

# Why3 Proof Results for Project "dfs"

## Theory "dfs.DFS": fully verified in 0.31 s

Obligations | Alt-Ergo (0.99.1) | Z3 (4.3.2) | ||

VC for dfs | --- | --- | ||

split_goal_wp | ||||

1. precondition | 0.01 | --- | ||

2. precondition | 0.01 | --- | ||

3. precondition | 0.00 | --- | ||

4. precondition | 0.02 | --- | ||

5. precondition | 0.01 | --- | ||

6. precondition | 0.02 | --- | ||

7. postcondition | 0.08 | --- | ||

8. postcondition | 0.02 | --- | ||

9. postcondition | 0.01 | --- | ||

10. postcondition | 0.01 | --- | ||

11. postcondition | 0.01 | --- | ||

12. postcondition | 0.01 | --- | ||

13. postcondition | 0.00 | --- | ||

14. postcondition | 0.01 | --- | ||

15. postcondition | 0.01 | --- | ||

16. postcondition | 0.01 | --- | ||

17. postcondition | 0.01 | --- | ||

reformulation | --- | --- | ||

induction_pr | ||||

1. | --- | --- | ||

simplify_trivial_quantification | ||||

1. | 0.00 | --- | ||

2. | --- | --- | ||

simplify_trivial_quantification | ||||

1. | --- | 0.00 | ||

VC for traverse | --- | --- | ||

split_goal_wp | ||||

1. assertion | 0.01 | --- | ||

2. precondition | 0.01 | --- | ||

3. precondition | 0.01 | --- | ||

4. precondition | 0.01 | --- | ||

5. postcondition | 0.01 | --- | ||

6. postcondition | 0.01 | --- | ||

7. postcondition | 0.00 | --- |