# Depth First Search (nbtw assumption)

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

• `vertices` : this constant is the set of graph vertices
• `successor` : this function gives for each vertex the set of vertices directly joinable from it
The algorithm is standard with gray/black sets of nodes. (white set is the union of their complements)
All proofs automatic, except Coq used to prove inductive post-condition of `dfs_main` via lemma `no_black_to_white_nopath`

```
module Dfs_nbtw
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
use import init_graph.GraphSetSuccPath

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

predicate white_monotony (v1 v2: set vertex) =
forall x: vertex. white_vertex x v2 -> white_vertex x v1

predicate nodeflip (x: vertex) (v1 v2: set vertex) =
white_vertex x v1 /\ not (white_vertex x v2)

predicate whitepath (x: vertex) (l: list vertex) (z: vertex) (v: set vertex) =
path x l z /\ (forall y. L.mem y l -> white_vertex y v) /\ white_vertex z v

lemma whitepath_mem_decomp:
forall x l1 l2 z y v. whitepath x (l1 ++ (Cons y l2)) z v -> whitepath x l1 y v /\ whitepath y (Cons y l2) z v

lemma whitepath_mem_decomp_right:
forall x l z y v. whitepath x l z v -> L.mem y (l ++ (Cons z Nil)) -> exists l': list vertex. whitepath y l' z v

predicate nodeflip_whitepath (roots v1 v2: set vertex) =
forall z. nodeflip z v1 v2 -> exists x l. mem x roots /\ whitepath x l z v1

predicate whitepath_nodeflip (roots v1 v2: set vertex) =
forall x l z. mem x roots -> whitepath x l z v1 -> nodeflip z v1 v2

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

lemma reachable_succ:
forall x x'. edge x x' -> reachable x x'

lemma reachable_trans:
forall x y z. reachable x y -> reachable y z -> reachable x z

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

lemma access_monotony_l:
forall roots roots' b. subset roots roots' -> access roots b -> access roots' b

lemma access_monotony_r:
forall roots b b'. subset b b' -> access roots b' -> access roots b

lemma access_trans:
forall roots b b'. access roots b' -> access b' b -> access roots b

predicate no_black_to_white (blacks grays: set vertex) =
forall x x'. edge x x' -> mem x blacks -> mem x' (union blacks grays)

lemma black_to_white_path_goes_thru_gray:
forall grays blacks. no_black_to_white blacks grays ->
forall x l "induction" z. path x l z -> mem x blacks -> not mem z (union blacks grays) ->
exists y. L.mem y l /\ mem y grays

```

### program

```
let rec dfs (roots grays blacks: set vertex): set vertex
variant {(cardinal vertices - cardinal grays), (cardinal roots)} =
requires {subset roots vertices}
requires {subset grays vertices}
requires {no_black_to_white blacks grays}
ensures {subset blacks result}
ensures {no_black_to_white result grays}
ensures {forall x. mem x roots -> not mem x grays -> mem x result}
ensures {access (union blacks roots) result}

if is_empty roots then blacks
else
let x = choose roots in
let roots' = remove x roots in
if mem x (union grays blacks) then
dfs roots' grays blacks
else
let b = dfs (successors x) (add x grays) blacks in
assert{ access (add x blacks) b};
dfs roots' grays (union blacks (add x b))

let dfs_main (roots: set vertex) : set vertex =
requires {subset roots vertices}
ensures {whitepath_nodeflip roots empty result}
ensures {nodeflip_whitepath roots empty result}
dfs roots empty empty

```

Thus the result of `dfs_main` is exactly the set of nodes reachable from `roots`

```
end
```

Generated by why3doc 0.86.1