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 soundness proof is adapted from Dowek and Munoz and is fully automatic. In this version, we use inductive predicates.

```
module Dfs_nbtw
use import int.Int
use import init_graph.GraphSetSucc

inductive reachable vertex vertex =
| Reachable_empty:
forall x: vertex. reachable x x
| Reachable_cons:
forall x y z: vertex.
edge x y -> reachable y z -> reachable x z

(*  predicate reachable (x z: vertex) =
exists l. path x l z  *)

lemma reachable_succ:
forall x x'. edge x x' -> reachable x x'

lemma reachable_trans:
forall x y z. reachable x y -> reachable y z -> reachable x z

inductive d_reach vertex vertex (set vertex) =
| d_access_empty:
forall x: vertex, v: set vertex.
not mem x v -> d_reach x x v
| d_access_cons:
forall x y z: vertex, v: set vertex.
not mem x v -> edge x y -> d_reach y z v -> d_reach x z v

lemma d_reach_monotony_r:
forall x z v v'. subset v v' -> d_reach x z v' -> d_reach x z v

lemma d_reach_reachable:
forall x z. reachable x z <-> d_reach x z empty

```

program

```
let rec random_search r v =
requires {subset (union r v) vertices}
ensures {subset v result}
ensures {forall z. mem z (diff result v) -> exists y. mem y r /\ d_reach y z 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
(*----------- nodeflip_whitepath -----------*)
assert {forall z. mem z (diff v' v) -> z <> x ->
(exists y. mem y r'/\ (d_reach y z v by d_reach y z (add x v)))
\/ ((d_reach x z v) by exists y'. mem y' (successors x) /\ d_reach y' z (add x v))};
v'

let random_search_main roots =
requires {subset roots vertices}
ensures {forall z. mem z result -> exists y. mem y roots /\ reachable y z}
random_search roots empty

```

Thus the result of `dfs_main` is exactly the set of nodes reachable from `roots`

```
(*  variant {(cardinal vertices - cardinal v), (cardinal r)} = *)
(*  ensures {result == union v (SC.filter (\ z. exists x. mem x r /\ d_reach x z v) vertices  )} *)

end

```

[session]

Generated by why3doc 0.88.3