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
• `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.
The new visited vertices are reachable by a white path w.r.t the old visited set.
Fully automatic proof, with inductive definition of white paths.

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.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

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

lemma whiteaccess_covar1:
forall r s s' v. subset s s' -> whiteaccess r s' v -> whiteaccess r s 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 s v v'. subset v v' -> whiteaccess r s v' -> whiteaccess r s 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 s t v. whiteaccess r s v -> whiteaccess s t v -> whiteaccess r t v

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

```

### program

```
let rec dfs r v
variant {(cardinal vertices - cardinal v), (cardinal r)} =
requires {subset r vertices }
requires {subset v vertices }
ensures {subset v result }
ensures {subset result vertices }
ensures {whiteaccess r (diff result v) 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
by whiteaccess (successors x) (diff v' (add x v)) v
by subset (diff v' (add x v)) (diff v' v)
by subset v (add x v) };
assert {whiteaccess (add x empty) (diff v' v) v
by diff v' v == add x (diff v' (add x v)) };
let v'' = dfs r' v' in
assert {whiteaccess r' (diff v'' v') v
by subset v v' };
assert {diff v'' v == union (diff v'' v') (diff v' v) };
v''

let dfs_main roots =
requires {subset roots vertices}
ensures {whiteaccess roots result empty
so  forall z. mem z result -> exists y l. mem y roots /\ path y l z }
dfs roots empty

end

```

#### [session]   [zip]

Generated by why3doc 0.88.3