why3doc index index

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

```
module RandomSearch
use import int.Int
use import list.List
use import list.Append
use import list.Mem as L
use import init_graph.GraphSetSucc
use import list.NumOcc

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 path_decomp_with_last_occ:
forall x z l1 l2 y. path x (l1 ++ (Cons y l2)) z -> y <> z -> exists l3 l4. l1 ++ (Cons y l2) = l3 ++ (Cons y l4) /\ not L.mem y l4

lemma whitepath_decomp_with_last_occ:
forall x z l1 l2 y v. whitepath x (l1 ++ (Cons y l2)) z v -> y <> z -> exists l. whitepath y (Cons y l) z v /\ not L.mem y l

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

```

### program

```
let rec random_search r v =
requires {subset r vertices }
requires {subset v vertices }
ensures {subset v result}
ensures {forall z y l. mem y r -> whitepath y l z v -> mem z (diff result v)}

if is_empty r then v else
let x = choose r in
let r' = remove x r in
if mem x v then random_search r' v else
let v' = random_search (union r' (successors x)) (add x v) in
(*----------- whitepath_nodeflip -----------*)
assert {forall z y l. mem y r -> whitepath y l z v -> z <> x ->
whitepath y l z (add x v) \/
exists x' l'. mem x' (successors x) /\ whitepath x' l' z (add x v) } ;
v'

let random_search_main (roots: set vertex) =
requires {subset roots vertices}
ensures {forall z y l. mem y roots -> path y l z -> mem z result}
random_search roots empty

end

```

#### [session]

Generated by why3doc 0.88.3