why3doc index index

Random search in graph

The graph is represented by a pair (vertices, successor)

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 wreach vertex vertex (set vertex) =
  | wReach_empty:
      forall x: vertex, v: set vertex. 
      not mem x v -> wreach x x v
  | wReach_cons:
      forall x y z: vertex, v: set vertex.
      not mem x v -> edge x y -> wreach y z v -> wreach x z v

  lemma wreach_var:
    forall x z v v'. subset v v' -> wreach x z v' -> wreach x z v

  lemma wreach_reachable:
    forall x z. reachable x z <-> wreach x z empty


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 /\ wreach 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
  assert {forall z. mem z (diff v' v) -> z <> x ->
                  (exists y. mem y r'/\ (wreach y z v by wreach y z (add x v)))
     \/ ((wreach x z v) by exists x'. edge x x' /\ wreach x' z (add x 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



Generated by why3doc 0.88.3