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.
The 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 list.Elements as E
use import init_graph.GraphSetSucc
use import init_graph.GraphSetSuccPath

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

forall x y l' z v. whitepath y l' z (add x v) <-> y <> x /\ not L.mem x l' /\ z <> x /\ whitepath y l' z v

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
variant {(cardinal vertices - cardinal v), (cardinal r)} =
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

Generated by why3doc 0.88.0