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 completeness proof is fully automatic.

module Dfs_stack2
use import int.Int
use import ref.Ref
use import list.List
use import list.Append
use import list.Mem as L
use import list.Elements as E
use import stack.Stack
use import list.NumOcc
use import init_graph.GraphSetSucc

lemma path_lst_occ:
forall x y z l. L.mem x l -> path y l z ->
exists l1 l2. l = l1 ++ Cons x l2 /\ path x (Cons x l2) z /\ not L.mem x l2

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

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_suffix:
forall x y z v l1 l2. whitepath y (l1 ++ Cons x l2) z v -> whitepath x (Cons x l2) z v

lemma whitepath_inv:
forall x z l v. whitepath x (Cons x l) z v -> not L.mem x l -> z <> x -> exists x'. edge x x' /\ whitepath x' l z (add x v)

lemma whitepath_split_lst_occ:
forall x y l z v. L.mem x l -> whitepath y l z v -> z <> x ->
exists x' l'. edge x x' /\ whitepath x' l' z (add x 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 y l. L.mem y (old r).elts -> whitepath y l z v -> mem z (diff result v)}

'L0:
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);
assert {forall z y l. L.mem y (at r 'L0).elts -> whitepath y l z v ->
z = x \/ whitepath y l z (add x v) \/
exists x' l'. edge x x' /\ whitepath x' l' z (add x v) } ;
end

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

end

#### [session]

Generated by why3doc 0.88.3