# DFS in graph (array + lists)

The graph is represented by array (list of successors)

• another proof with paths only
The algorithm is depth-first-search in the graph. It picks the first son in list of successors and makes recursive call with it.
The proof is mutually recursive on pre and post conditions. Fully automatic proof.

```module GraphArraySucc
use import int.Int
use import array.Array
use import list.List
use import list.Mem
use import list.NumOcc
use import list.Append

type graph = array (list int)
predicate spl (lv: list int) = forall x: int. mem x lv -> num_occ x lv = 1

function order (g: graph) : int = length g
predicate vertex (g: graph) (x: int) = 0 <= x < order g
predicate out (g: graph) (x: int)  = forall y: int. vertex g x -> mem y g[x] -> vertex g y
predicate wf (g: graph) = forall x: int. vertex g x -> out g x
predicate edge (x y: int) (g: graph) = vertex g x /\ mem y g[x]

lemma mem_decidable:
forall x: int, lv: list int. mem x lv \/ not mem x lv

lemma spl_single:
forall x: int. spl (Cons x Nil)

lemma spl_expansion:
forall x: int, l: list int. spl l -> not (mem x l) -> spl (l ++ (Cons x Nil))

lemma spl_sub:
forall lv lv1 lv2: list int. lv = lv1 ++ lv2 -> spl lv -> spl lv1 /\ spl lv2

end

module GraphArraySuccPath
use import GraphArraySucc
use import int.Int
use import array.Array
use import list.List
use import list.Mem
use import list.Append

inductive path int (list int) int graph =
| Path_empty:
forall x: int, g: graph. vertex g x -> path x Nil x g
| Path_cons:
forall x y z: int, l: list int, g: graph.
edge x y g -> path y l z g -> path x (Cons x l) z g

predicate path_fst_not_twice (x z: int) (l: list int) (g: graph) =
path x (Cons x l) z g /\ (not mem x l)

lemma path_edge:
forall x z: int, g: graph. path x (Cons x Nil) z g -> edge x z g

lemma path_hd:
forall x y z: int, l: list int, g: graph. path x (Cons y l) z g -> x = y

lemma path_right_extension:
forall x y z: int, l: list int, g: graph.
wf g -> path x l y g -> edge y z g -> path x (l ++ Cons y Nil) z g

lemma path_right_inversion:
forall x z: int, l: list int, g: graph. path x l z g ->
(x = z /\ l = Nil)
\/ (exists y: int, l': list int.
path x l' y g /\ edge y z g /\ l = l' ++ Cons y Nil)

lemma path_trans:
forall x y z: int, l1 l2: list int, g: graph.
path x l1 y g -> path y l2 z g -> path x (l1 ++ l2) z g

lemma empty_path:
forall x z: int, g: graph. path x Nil z g -> x = z

lemma path_decomposition:
forall x y z: int, l1 l2: list int, g: graph.
path x (l1 ++ Cons y l2) z g -> path x l1 y g /\ path y (Cons y l2) z g

lemma path_vertex_l :
forall x y z: int, l : list int, g : graph.
wf g -> vertex g x -> path x l z g -> mem y l -> vertex g y

lemma path_vertex_r :
forall x z : int, l : list int, g : graph.
wf g -> vertex g x -> path x l z g -> vertex g z

lemma path_vertex_last_occ :
forall x y z: int, l : list int, g: graph.
path x l z g -> mem y l ->
(exists l1 l2 : list int. l = l1 ++ (Cons y l2) /\ (path_fst_not_twice y z l2 g))
end

module GraphArraySuccPathColored
use import GraphArraySucc
use import GraphArraySuccPath
use import int.Int
use import array.Array
use import list.List
use import list.Mem
use import list.Append

type color = WHITE | GRAY | BLACK

predicate whitepath (x: int) (l: list int) (z: int) (g: graph) (c: array color) =
path x l z g /\ c[x] = WHITE = c[z] /\ (forall y: int. mem y l -> c[y] = WHITE)

predicate node_flip (x: int) (c1 c2: array color) =
c1[x] = WHITE /\ c2[x] <> WHITE

predicate whitepath_flip (x z: int) (l: list int) (g: graph) (c1 c2: array color) =
whitepath x l z g c1 /\ not whitepath x l z g c2

lemma whitepath_trans:
forall x y z: int, l1 l2: list int, g: graph, c: array color.
whitepath x l1 y g c -> whitepath y l2 z g c -> whitepath x (l1 ++ l2) z g c

lemma whitepath_mem_decomp:
forall x y z: int, l: list int, g: graph, c: array color.
whitepath x l z g c -> mem y l ->
(exists l1 l2 : list int. l = l1 ++ (Cons y l2) /\ whitepath x l1 y g c /\ whitepath y (Cons y l2) z g c)

lemma whitepath_mem_decomp_right:
forall x y z: int, l: list int, g: graph, c: array color.
wf g -> vertex g x -> whitepath x l z g c -> mem y (l ++ (Cons z Nil)) ->
exists l': list int. whitepath y l' z g c

lemma whitepathflip_contains_node_flip:
forall x z: int, l: list int, g: graph, c1 c2: array color.
wf g -> vertex g x -> whitepath_flip x z l g c1 c2 ->
exists y: int. vertex g y /\ mem y (l ++ (Cons z Nil)) /\ node_flip y c1 c2

lemma whitepathflip_contains_node_flip_whitepath:
forall x z: int, l: list int, g: graph, c1 c2: array color.
wf g -> vertex g x -> whitepath_flip x z l g c1 c2 ->
exists y: int, l': list int. vertex g y /\ mem y (l ++ (Cons z Nil)) /\ node_flip y c1 c2 /\ whitepath y l' z g c1

lemma whitepath_whitepostfix :
forall x z : int, l: list int, g: graph, c : array color.
wf g -> vertex g x -> whitepath x l z g c -> x <> z ->
(exists y: int, l': list int. edge x y g /\ whitepath y l' z g (set c x GRAY))

end

module Dfs

use import int.Int
use import ref.Ref
use import array.Array
use import list.List
use import list.Mem
use import list.HdTlNoOpt
use import list.NthNoOpt
use import list.Append
use import list.Reverse
use import GraphArraySucc
use import GraphArraySuccPath
use import GraphArraySuccPathColored

predicate white_monotony (g: graph) (c1 c2: array color) =
forall x: int. vertex g x -> c2[x] = WHITE -> c1[x] = WHITE

predicate whitepath_monotony (g: graph) (c1 c2: array color) =
forall x z: int, l: list int. vertex g x -> whitepath x l z g c2 -> whitepath x l z g c1

predicate node_flip_whitepath (x: int) (g: graph) (c1 c2: array color) =
forall z: int. node_flip z c1 c2 -> exists l: list int. whitepath x l z g c1

predicate whitepath_node_flip (x: int) (g: graph) (c1 c2: array color) =
forall z: int, l: list int. whitepath x l z g c1 -> node_flip z c1 c2

predicate node_flip_whitepath_in_list (lv: list int) (g: graph) (c1 c2: array color) =
forall z: int. node_flip z c1 c2 ->
exists x: int, l': list int. mem x lv /\ whitepath x l' z g c1

predicate whitepath_in_list_node_flip (lv: list int) (g: graph) (c1 c2: array color) =
forall x: int. mem x lv -> whitepath_node_flip x g c1 c2

predicate whitepath_flip_whitepath (x: int) (g: graph) (c1 c2: array color) =  (*new*)
forall y z: int, l: list int. whitepath_flip y z l g c1 c2 ->
exists l': list int. whitepath x l' z g c1

predicate whitepath_flip_whitepath_in_list (lv: list int) (g: graph) (c1 c2: array color) =  (*new*)
forall x z: int, l: list int. whitepath_flip x z l g c1 c2 ->
exists x': int, l': list int. mem x' lv /\ whitepath x' l' z g c1

predicate whitepath_cons (x: int) (g: graph) (c1 c2: array color) =
forall y z: int, l: list int. mem y g[x] ->
whitepath y l z g c2 -> whitepath x (Cons x l) z g c1

lemma flip_case :
forall x z: int, c1 c2: array color.
node_flip z c1 (set c2 x BLACK) -> node_flip z (set c1 x GRAY) c2 \/ z = x

```

### program

```let rec dfs (g: graph) (x: int) (c: array color) =
requires {wf g /\ vertex g x /\ Array.length c = order g}
requires {c[x] = WHITE}
ensures {white_monotony g (old c) c}
ensures {node_flip_whitepath x g (old c) c && whitepath_flip_whitepath x g (old c) c}
ensures {whitepath_node_flip x g (old c) c}

'L0:
c[x] <- GRAY;
assert {whitepath_cons x g (at c 'L0) c};
'L:
let sons = ref (g[x]) in
let ghost lv = ref Nil in
while  ( !sons <> Nil) do
invariant {(reverse !lv) ++ !sons = g[x]}
invariant {white_monotony g (at c 'L) c}
invariant {whitepath_monotony g (at c 'L) c}
invariant {whitepath_flip_whitepath_in_list !lv g (at c 'L) c}
invariant {node_flip_whitepath_in_list !lv g (at c 'L) c}
invariant {whitepath_in_list_node_flip !lv g (at c 'L) c}

'L1:
match !sons with
| Nil -> ()
| Cons y sons' ->
if c[y] = WHITE then begin
dfs g y c;
end;
sons := sons';
lv := Cons y !lv
end
done;
c[x] <- BLACK

let dfs_main (g: graph) =
requires { wf g }
let n = length (g) in
let c = make n WHITE in
for i = 0 to n - 1 do
if c[i] = WHITE then
dfs g i c
done

end
```

Generated by why3doc 0.86.1