why3doc index index

# DFS in graph - soundness of the whitepath theorem

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

• `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 depth-first-search in the graph as described in Sedgewick (Algorithms). It picks randomly the son on which recursive call is done.
This theorem refers to the whitepath theorem in Cormen et al.
The new visited vertices are reachable by a white path w.r.t the old visited set.
Quasi automatic proof, with inductive definition of white paths, mutable set of visited vertices, black/white color. The proof is similar to the functional one. One loop invariant (the whiteaccess invariant) is proved in Coq.

Notice that this proof uses paths.

```
module DfsWhitePathSoundness
use import int.Int
use import list.List
use import list.Append
use import list.Mem as L
use import list.Length
use import list.HdTlNoOpt
use import list.Reverse
use import list.Elements as E
use import array.Array
use import ref.Ref
use import init_graph.GraphListArraySucc

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 (roots b v: set vertex) =
forall z. mem z b -> exists x l. mem x roots /\ wpath x l z v

lemma whiteaccess_var:
forall r r' b v. subset r r' -> whiteaccess r b v -> whiteaccess r' b v

lemma whiteaccess_covar1:
forall r b b' v. subset b b' -> whiteaccess r b' v -> whiteaccess r b v

lemma wpath_covar2:
forall x l z v v'. subset v v' -> wpath x l z v' -> wpath x l z v

lemma whiteaccess_covar2:
forall r b v v'. subset v v' -> whiteaccess r b v' -> whiteaccess r b v

lemma wpath_trans:
forall x l y l' z v. wpath x l y v -> wpath y l' z v -> wpath x (l ++ l') z v

lemma whiteaccess_trans:
forall r r' b v. whiteaccess r r' v -> whiteaccess r' b v -> whiteaccess r b v

lemma whiteaccess_cons:
forall x s v. mem x vertices ->
white_vertex x v -> whiteaccess (elements (successors x)) s v -> whiteaccess (add x empty) s v

lemma whiteaccess_union:
forall r b1 b2 v. whiteaccess r (union b1 b2) v <-> whiteaccess r b1 v /\ whiteaccess r b2 v

lemma path_wpathempty:
forall y l z. wpath y l z empty -> path y l z

lemma diff_inc:
forall a b c: set 'alpha. subset c b -> subset b a -> diff a c = union (diff a b) (diff b c)
by diff a c == union (diff a b) (diff b c)

```

### program

```  type color = WHITE | GRAY | BLACK

let rec dfs1 x col graph (ghost v) =
requires {Array.length graph = Array.length col = cardinal vertices}
requires {forall x. graph[x] = successors x}
requires {mem x vertices /\ col[x] = WHITE}
requires {forall x. mem x !v <-> mem x vertices /\ col[x] <> WHITE}
ensures {forall x. mem x !v <-> mem x vertices /\ col[x] <> WHITE}
ensures {subset !(old v) !v }
ensures {whiteaccess (add x empty) (diff !v !(old v)) !(old v) }
'L0:
let ghost v0 = !v in
let ghost col0 = Array.copy col in
assert {not mem x v0};
col[x] <- GRAY; v := add x !v;
let sons = ref graph[x] in
let ghost dejavu = ref Nil in
while !sons <> Nil do
invariant {subset (elements !sons) vertices}
invariant {subset !v vertices}
invariant {forall z. mem z !v <-> mem z vertices /\ col[z] <> WHITE}
invariant {whiteaccess (elements !dejavu) (diff !v (add x v0)) v0}
invariant {subset (add x v0) !v}
invariant {successors x = (reverse !dejavu) ++ !sons}
let y = hd !sons in
if col[y] = WHITE then dfs1 y col graph v;
sons := tl !sons;
dejavu := Cons y !dejavu;
done;
'L1:
let ghost v' = !v in
by whiteaccess (elements (successors x)) (diff v' (add x v0)) v0 };
assert {wpath x Nil x v0};
assert {whiteaccess (add x empty) (diff v' v0) v0
by diff v' v0 == add x (diff v' (add x v0))
by mem x v'};
col[x] <- BLACK

let dfs_main roots graph =
requires {Array.length graph = cardinal vertices}
requires {forall x. graph[x] = successors x}
requires {subset (elements roots) vertices}
ensures {whiteaccess (elements roots) (elements result) empty
so  forall z. mem z (elements result) -> exists x l. mem x (elements roots) /\ path x l z }
let n = Array.length graph in
let col = Array.make n WHITE in
let ghost v = ref empty in
let xs = ref roots in
let ghost dejavu = ref Nil in
while !xs <> Nil do
invariant {subset (elements !xs) vertices}
invariant {subset !v vertices}
invariant {forall z. mem z !v <-> mem z vertices /\ col[z] <> WHITE}
invariant {whiteaccess (elements !dejavu) !v empty}
invariant {roots = (reverse !dejavu) ++ !xs}
let x = hd !xs in
if col[x] = WHITE then dfs1 x col graph v;
xs := tl !xs;
dejavu := Cons x !dejavu;
done;
let res = ref Nil in
for x = 0 to n - 1  do
invariant {forall y. L.mem y !res <-> 0 <= y < x /\ col[y] <> WHITE}
if col[x] <> WHITE then res := Cons x !res
done;
!res

```

```
```

#### extracted program

```
(* let rec dfs1 x col graph =
col[x] <- GRAY;
let sons = ref graph[x] in
while !sons <> Nil do
let y = hd !sons in
if col[y] = WHITE then dfs1 y col graph;
sons := tl !sons;
done;
col[x] <- BLACK

let dfs_main roots graph =
let n = Array.length graph in
let col = Array.make n WHITE in
let xs = ref roots in
while !xs <> Nil do
let y = hd !xs in
if col[y] = WHITE then dfs1 y col;
xs := tl !xs;
done;
let res = ref Nil in
for x = 0 to n - 1  do
if col[x] <> WHITE then res := Cons x !res
done;
!res
*)

end
```

Generated by why3doc 0.88.3