why3doc index index

# DFS in graph - completeness of the whitepath theorem

The graph is represented by a pair (`vertices`, `successors`)

• `vertices` : this constant is the set of graph vertices
• `successors` : this function gives for each vertex the set of vertices directly joinable from it
The algorithm is depth-first-search in the graph. It picks randomly the son on which recursive call is done.
This theorem refers to the whitepath theorem in Cormen et al.
Every vertex reachable by a white path (w.r.t the old visited set) is in the result
Fully automatic proof, with inductive definition of white paths. For the main program, a Coq proof is needed to prove equivalence between inductive predicate `wpath` and universal definition of white path with `path` predicate.

Notice that this proof does not use paths.

```
module DfsWhitePathCompleteness
use import int.Int
use import list.List
use import list.Append
use import list.Mem as L
use import list.Elements as E
use import init_graph.GraphSetSucc

predicate white_vertex (x: vertex) (v: set vertex) =
not (mem x v)

inductive wpath vertex (list vertex) vertex (set vertex) =
| WPath_empty:
forall x v. white_vertex x v -> wpath x Nil x v
| WPath_cons:
forall x y l z v.
white_vertex x v -> edge x y -> wpath y l z v -> wpath x (Cons x l) z v

predicate whiteaccess (r s v: set vertex) =
forall z. mem z s -> exists x l. mem x r /\ wpath x l z v

predicate nbtw (r v: set vertex) =
forall x x'. edge x x' -> mem x r -> mem x' (union r v)

lemma nbtw_path:
forall v v'. nbtw (diff v' v) v' ->
forall x l z. mem x (diff v' v) -> wpath x l z v -> mem z (diff v' v)

```

### program

```
let rec dfs r v
variant {(cardinal vertices - cardinal v), (cardinal r)} =
requires {subset r vertices }
requires {subset v vertices }
ensures {subset result vertices }
ensures {subset v result }
ensures {subset r result }
ensures {nbtw (diff result v) v &&
forall s. whiteaccess r s v -> subset s (diff result v) }
if is_empty r then v else
let x = choose r in
let r' = remove x r in
if mem x v then dfs r' v else
let v' = dfs (successors x) (add x v) in
assert {diff v' v == add x (diff v' (add x v)) };
let v'' = dfs r' v' in
assert {diff v'' v == union (diff v'' v') (diff v' v) };
v''

lemma path_wpath:
forall x l z v. wpath x l z v <->
path x l z /\ forall y. L.mem y (l ++ Cons z Nil) -> not mem y v

predicate reachable (x z: vertex) =
exists l. path x l z

predicate access (r s: set vertex) = forall z. mem z s -> exists x. mem x r /\ reachable x z

lemma path_wpath_empty:
forall x l z. path x l z <-> wpath x l z empty

lemma access_whitepath_empty:
forall r s. access r s <-> whiteaccess r s empty

let dfs_main roots =
requires {subset roots vertices}
ensures {forall s. access roots s -> subset s result}
dfs roots empty

end

```

#### [session]   [zip]

Generated by why3doc 0.88.3