# Iterative depth first search with stack

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 a ministep of a random search in the graph. It is generic to any search strategy.
The proof is adapted from Dowek and Munoz and is fully automatic.

```
module Dfs_stack
use import int.Int
use import ref.Ref
use import list.List
use import list.Length
use import list.Mem as L
use import list.Elements as E
use import list.Append
use import stack.Stack
use import init_graph.GraphSetSucc
use import init_graph.GraphSetSuccPath

predicate white_vertex (x: vertex) (v: set vertex) =
not (mem x v)

predicate nodeflip (x: vertex) (v1 v2: set vertex) =
white_vertex x v1 /\ not (white_vertex x v2)

predicate whitepath (x: vertex) (l: list vertex) (z: vertex) (v: set vertex) =
path x l z /\ (forall y. L.mem y l -> white_vertex y v) /\ white_vertex z v

predicate whiteaccess (r: set vertex) (z: vertex) (v: set vertex) =
exists x l. mem x r /\ whitepath x l z v

predicate path_fst_not_twice (x: vertex) (l: list vertex) (z: vertex) =
path x l z /\
match l with
| Nil -> true
| Cons _ l' -> x <> z /\ not (L.mem x l')
end

lemma path_suffix_fst_not_twice:
forall x z l "induction". path x l z ->
exists l1 l2. l = l1 ++ l2 /\ path_fst_not_twice x l2 z

lemma path_path_fst_not_twice:
forall x z l. path x l z ->
exists l'. path_fst_not_twice x l' z /\ subset (E.elements l') (E.elements l)

predicate whitepath_fst_not_twice (x: vertex) (l: list vertex) (z: vertex) (v: set vertex) =
whitepath x l z v /\ path_fst_not_twice x l z

lemma whitepath_decomposition:
forall x l1 l2 z y v. whitepath x (l1 ++ (Cons y l2)) z v -> whitepath x l1 y v /\ whitepath y (Cons y l2) z v

lemma whitepath_mem_decomposition_r:
forall x l z y v. whitepath x l z v -> L.mem y (l ++ (Cons z Nil)) -> exists l': list vertex. whitepath y l' z v

lemma whitepath_whitepath_fst_not_twice:
forall x z l v. whitepath x l z v -> exists l'. whitepath_fst_not_twice x l' z v

lemma path_cons_inversion:
forall x z l. path x (Cons x l) z -> exists y. edge x y /\ path y l z

lemma whitepath_cons_inversion:
forall x z l v. whitepath x (Cons x l) z v -> exists y. edge x y /\ whitepath y l z v

lemma whitepath_cons_fst_not_twice_inversion:
forall x z l v. whitepath_fst_not_twice x (Cons x l) z v -> x <> z ->
(exists y. edge x y /\ whitepath y l z (add x v))

lemma whitepath_fst_not_twice_inversion :
forall x z l v. whitepath_fst_not_twice x l z v -> x <> z ->
(exists y l'. edge x y /\ whitepath y l' z (add x v))

predicate nodeflip_whitepath (roots v1 v2: set vertex) =
forall z. nodeflip z v1 v2 -> whiteaccess roots z v1

predicate whitepath_nodeflip (roots v1 v2: set vertex) =
forall x l z. mem x roots -> whitepath x l z v1 -> nodeflip z v1 v2

```

### program

```
let rec push_set (p: Stack.t vertex) (s: set vertex)
variant { cardinal s } =
ensures { union (elements (old p.elts)) s == elements p.elts }
if not is_empty s then begin
let x = choose s in
Stack.push x p;
push_set p (remove x s)
end

let rec dfs (roots: Stack.t vertex) (visited: set vertex): set vertex
variant {(cardinal vertices - cardinal visited), L.length (roots.elts)} =
requires {subset (elements (roots.elts)) vertices }
requires {subset visited vertices }
raises {Empty}
ensures {subset visited result}
ensures {whitepath_nodeflip (elements (old roots.elts)) visited result}
ensures {nodeflip_whitepath (elements (old roots.elts)) visited result}
'L0:
if Stack.is_empty roots then
visited
else
let x = Stack.pop roots in
'L1:
if mem x visited then
dfs roots visited
else begin
push_set roots (successors x);
'L2:
let r = dfs roots (add x visited) in
(*----------- nodeflip_whitepath -----------*)
assert {forall z. nodeflip z visited r -> z = x \/ nodeflip z (add x visited) r };
(* case 1-1: nodeflip z visited r /\ z = x *)
assert {whitepath x Nil x visited};
(* case 1-2: nodeflip z visited r /\ z <> x *)
assert {let roots' = elements (at roots.elts 'L1) in
forall z. nodeflip z (add x visited) r -> whiteaccess roots' z (add x visited)
\/ whiteaccess (successors x) z (add x visited)};
assert {forall x' l z. whitepath x' l z (add x visited) -> whitepath x' l z visited};
assert {forall z x' l. edge x x' -> whitepath x' l z visited -> whitepath x (Cons x l) z visited};
assert {subset (elements (at roots.elts 'L1))(elements (at roots.elts 'L0))};
assert {subset (elements (at roots.elts 'L2))(union (elements (at roots.elts 'L1)) (successors x))};
assert {forall z. nodeflip z (add x visited) r -> whiteaccess (elements (at roots.elts 'L0)) z visited};

(*-------------- whitepath_nodeflip -------------*)

(* case 1: whitepath x l z visited /\ x = z *)
assert {mem x r};

(* case 2: whitepath x l z /\ x <> z *)
(* using lemma whitepath_whitepath_fst_not_twice *)
assert {forall l z. whitepath x l z visited -> x <> z
-> exists x' l'. edge x x' /\ whitepath x' l' z (add x visited)};
(* same as lemma whitepath_inversion *)
assert {forall l z. whitepath x l z visited -> x <> z -> nodeflip z (add x visited) r};
assert {forall l z. whitepath x l z visited -> nodeflip z visited r};

(* case 3: whitepath roots' l z *)
(* case 3-1: whitepath roots' l z /\ L.mem x l *)
assert {forall y l z. whitepath y l z visited -> (L.mem x l \/ x = z)
-> exists l'. whitepath x l' z visited};
(* goto cases 1-2 *)
(* case 3-2: whitepath roots' l z /\ not (L.mem x l) *)
assert {let roots' = elements (at roots.elts 'L1) in
forall y l z. mem y roots' -> whitepath y l z visited -> not (L.mem x l \/ x = z)
-> whitepath y l z (add x visited)};
r
end

let dfs_main (roots: Stack.t vertex) =
requires {subset (elements (roots.elts)) vertices}
raises {Empty}
dfs roots empty

end
```

Generated by why3doc 0.86.1