why3doc index index

# DFS in undirected graph - there is no edge from white vertex to black vertex

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
We show that in a undirected graph, the is no edge from a white vertex to a black vertex.
Fully automatic proof, with inductive definition of white paths.

```
module DfsUndirNoWhiteToBlack
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

axiom undirected_graph:
forall x y. edge x y -> edge y x

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

predicate nwtb (b g: set vertex) =
forall x x'. edge x x' -> mem x' b -> mem x (union b g)

```

### program

```
let rec dfs r g b
variant {(cardinal vertices - cardinal g), (cardinal r)} =
requires {subset r vertices }
requires {subset b vertices }
requires {subset g vertices }
requires {inter b g == empty}
ensures {subset result vertices }
ensures {subset b result }
ensures {inter result g == empty}
ensures {subset (diff r g) result &&
nbtw (diff result (union b g)) (union b g) &&
nwtb (diff result (union b g)) (union b g)}
if is_empty r then b else
let x = choose r in
let r' = remove x r in
let v = union b g in
if mem x v then dfs r' g b else
let v' = dfs (successors x) (add x g) b in
assert {diff (add x v') b == add x (diff v' b) };
let v'' = dfs r' g (add x v') in
assert {diff v'' b == union (diff v'' (add x v')) (diff (add x v') b) };
v''
end

```

#### [session]   [zip]

Generated by why3doc 0.88.3