why3doc index index

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)
The proof assumes to start with non black-to-white colouring.
All proofs automatic.

Program logic with `reachable` predicate defined with an existential quantifier, and `access` predicate.

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

(*  inductive reachable vertex vertex =
| Reachable_empty:
forall x: vertex. reachable x x
| Reachable_cons:
forall x y z: vertex.
edge x y -> reachable y z -> reachable x z
*)

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 (r s: set vertex) = forall z. mem z s -> exists x. mem x r /\ reachable x z

lemma access_var:
forall r r' s. subset r r' -> access r s -> access r' s

lemma access_covar:
forall r s s'. subset s s' -> access r s' -> access r s

lemma access_trans:
forall r s t. access r s -> access s t -> access r t

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

lemma black_to_white_path_goes_thru_gray:
forall g b. no_black_to_white b g ->
forall x l z. path x l z -> mem x b -> not mem z (union b g) ->
exists y. L.mem y l /\ mem y g

```

program

```
let rec dfs r g b
variant {(cardinal vertices - cardinal g), (cardinal r)} =
requires {subset r vertices}
requires {subset g vertices}
requires {no_black_to_white b g}
ensures {subset b result}
ensures {no_black_to_white result g}
ensures {forall x. mem x r -> not mem x g -> mem x result}
ensures {access (union b r) result}

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

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

```

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

```
end

```

[session]

Generated by why3doc 0.88.3