why3doc index index

# 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 iterative depth-first-search with a stack. The proof is quasi similar to random search.
This soundness proof 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

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

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

lemma whitepath_id:
forall x v. not mem x v -> whitepath x Nil x v

lemma whitepath_covar:
forall v v' x l y. subset v v' -> whitepath x l y v' -> whitepath x l y v

lemma whitepath_cons:
forall x x' y l v. not mem x v -> edge x x' -> whitepath x' l y v -> whitepath x (Cons x l) y v

```

### 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 r v
variant {(cardinal vertices - cardinal v), L.length (r.elts)} =
requires {subset (elements r.elts) vertices }
requires {subset v vertices }
ensures {subset v result }
ensures {subset result vertices }
raises {Empty}
ensures {subset v result}
ensures {forall z. mem z (diff result v) -> exists y l. L.mem y (old r).elts /\ whitepath y l z v}

if Stack.is_empty r then v else
let x = Stack.pop r in
'L1:
if mem x v then dfs r v else begin
push_set r (successors x);
let v' = dfs r (add x v) in
assert {forall z. mem z (diff v' v) -> z <> x ->
(exists y l. mem y (elements (at r 'L1).elts) /\ (whitepath y l z v by whitepath y l z (add x v)))
\/ ((exists l. whitepath x l z v)
by  exists x' l'. edge x x' /\ whitepath x' l' z v)};
v'
end

let dfs_main (roots: Stack.t vertex) =
requires {subset (elements (roots.elts)) vertices}
raises {Empty}
ensures {forall z. mem z result -> exists y l. L.mem y (old roots).elts /\ path y l z}
dfs roots empty

end

```

#### [session]

Generated by why3doc 0.88.3