# Random DFS in graph

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 depth-first-search in the graph. It picks randomly the son on which recursive call is done.
The proof is mutually recursive on pre and post conditions. Fully automatic proof.

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

lemma mem_decidable:
forall x: 'a, l: list 'a. L.mem x l \/ not L.mem x l

lemma list_suffix_fst_not_twice:
forall x, l "induction" : list vertex. L.mem x l -> exists l1 l2. l = l1 ++ (Cons x l2) /\ not L.mem x l2

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

predicate white_monotony (v1 v2: set vertex) =
forall x: vertex. white_vertex x v2 -> white_vertex x v1

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

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_mem_decomp:
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_decomp_right:
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

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 why_type_decidable:
forall x y: 'a. x = y \/ x <> y

lemma Lmem_decidable:
forall x:vertex, l. L.mem x l \/ not (L.mem x l)

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)

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_not_nil_inversion:
forall x z l. path x (Cons x l) z -> exists y. edge x y /\ path y l z

lemma whitepath_not_nil_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_not_nil_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: vertex, l': list vertex. edge x y /\ l = Cons x l' /\ whitepath y l' z (add x v))

lemma whitepath_inversion :
forall x z l v. whitepath x l z v -> x <> z ->
(exists y: vertex, l': list vertex. edge x y /\ whitepath y l' z (add x v))

lemma nodeflip_monotony :
forall x v0 v1 v2. subset v0 v1 -> nodeflip x v1 v2 -> nodeflip x v0 v2

lemma whitepath_monotony :
forall x l z v0 v1. subset v0 v1 -> whitepath x l z v1 -> whitepath x l z v0

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

lemma whitepath_trans:
forall x l y l' z v. whitepath x l y v -> whitepath y l' z v -> whitepath x (l ++ l') z v

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

lemma whitepath_flip_node_flip:
forall x l z v1 v2. whitepath x l z v1 -> not whitepath x l z (union v2 v1) -> exists y. L.mem y (l ++ (Cons z Nil)) /\ nodeflip y v1 v2

```

### program

```
let rec dfs (roots: set vertex) (visited: set vertex): set vertex
variant {(cardinal vertices - cardinal visited), (cardinal roots)} =
requires {subset roots vertices }
requires {subset visited vertices }
ensures {subset visited result}
ensures {subset result vertices}
ensures {nodeflip_whitepath roots visited result}
if is_empty roots then visited
else
let x = choose roots in
let roots' = remove x roots in
if mem x visited then
dfs roots' visited
else begin
let r' = dfs (successors x) (add x visited) in
let r = dfs roots' r' in
(*-------- nodeflip_whitepath ----------------------------*)
assert {forall z. nodeflip z visited r -> nodeflip z visited r' \/ nodeflip z r' r};
(*-------- case 1 ----------*)
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 {forall z. nodeflip z (add x visited) r' -> 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 {forall z. nodeflip z (add x visited) r' -> whiteaccess roots z visited};
(*-------- case 2 ------------*)
assert {forall z. nodeflip z r' r -> whiteaccess roots' z r'};
assert {forall z x' l. whitepath x' l z r' -> whitepath x' l z visited};

r
end

let dfs_main (roots: set vertex) : set vertex =
requires {subset roots vertices}
dfs roots empty

end
```

Generated by why3doc 0.86.1