why3doc index index

DFS in graph - soundness of the whitepath theorem

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

The algorithm is depth-first-search in the graph. It picks randomly the son on which recursive call is done.
This theorem refers to the whitepath theorem in Cormen et al.
The new visited vertices are reachable by a white path w.r.t the old visited set.
Fully automatic proof, with inductive definition of white paths and mutable set of visited vertices. The proof is similar to the functional one.

Notice that this proof uses paths.

module DfsWhitePathCopmleteness
  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 ref.Ref
  use import init_graph.GraphListSucc

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

  inductive wpath vertex (list vertex) vertex (set vertex) =
  | WPath_empty:
      forall x v. white_vertex x v -> wpath x Nil x v
  | WPath_cons:
      forall x y l z v.
      white_vertex x v -> edge x y -> wpath y l z v -> wpath x (Cons x l) z v

  predicate whiteaccess (roots b v: set vertex) =
    forall z. mem z b -> exists x l. mem x roots /\ wpath x l z v

  lemma whiteaccess_union:
    forall r b1 b2 v. whiteaccess r (union b1 b2) v <-> whiteaccess r b1 v /\ whiteaccess r b2 v

  predicate nbtw (b v: set vertex) =
    forall x x'. edge x x' -> mem x b -> mem x' (union b v)

  lemma nbtw_path:
    forall v v'. nbtw (diff v' v) v' -> 
      forall x l z. mem x (diff v' v) -> wpath x l z v -> mem z (diff v' v)


let rec dfs r (v : ref (set vertex)) =
  requires {subset (elements r) vertices }
  requires {subset !v vertices }
  ensures {subset !v vertices }
  ensures {subset !(old v) !v }
  ensures {subset (elements r) !v}
  ensures {nbtw (diff !v !(old v)) !v &&
           forall s. whiteaccess (elements r) s !(old v) -> subset s (diff !v !(old v)) }
  let ghost v0 = !v in
  match r with
  | Nil -> ()
  | Cons x r' ->  if mem x !v then dfs r' v else begin
  v := add x !v;
  dfs (successors x) v;
  let ghost v' = !v in
  assert {diff v' v0 == add x (diff v' (add x v0)) };
  dfs r' v;
  let ghost v'' = !v in
  assert {diff v'' v0 == union (diff v'' v') (diff v' v0) };


[session]   [zip]

Generated by why3doc 0.88.3