why3doc index index

DFS in graph - completeness of the whitepath theorem

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

This algorithm is depth-first-search in the graph. It picks randomly the son on which recursive call is done.
This theorem refers to the White-path theorem in book by Cormen et al.
The new visited vertices are exactly the ones reachable from roots by a white path w.r.t the previously visited set.
Automatic proof, with inductive definition of white paths and heavy use of the "by" connective.

Notice that this proof relies on the non-black-to-white property for its completeness.
The set of visited vertices is splitted into gray and black sets. Strangely, this proof is slightly more complex than with a sole set of visited vertices.

The formula "A && B" means "A /\ A -> B" .
The formula "A by B" means "B /\ B -> A"

module DFSWhitePathGrayCompteness
  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

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 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

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

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

  lemma whiteaccess_var:
    forall r r' b v. subset r r' -> whiteaccess r b v -> whiteaccess r' b v

  lemma whiteaccess_minus:
    forall r s v. whiteaccess r s v -> whiteaccess (diff r v) s v

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

  lemma nbtw_whiteaccess:
    forall r s v. nbtw (diff r v) v -> whiteaccess r s v -> subset s (diff r v)

  lemma diff_empty:
    forall b g r: set vertex. inter r g == empty -> diff r (union b g) == diff r b

   lemma whiteaccess_roots_result: 
   forall r r' s v b g. v = union b g -> subset (diff r g) r' -> whiteaccess r s v
     -> whiteaccess (diff r' v) s v
     by whiteaccess r' s v
     by whiteaccess (diff r g) s v
     by whiteaccess (diff r v) s v


let rec dfs r g b 
  variant {(cardinal vertices - cardinal g), (cardinal r)} =
  requires {subset r vertices }
  requires {subset b vertices }
  requires {subset g vertices }
  requires {inter b g == empty}
  ensures {subset result vertices }
  ensures {subset b result }
  ensures {inter result g == empty}
  ensures {subset (diff r g) result &&
           nbtw (diff result (union b g)) (union b g) &&
           forall s. whiteaccess r s (union b g) -> subset s (diff result b) }
  if is_empty r then b else
  let x = choose r in
  let r' = remove x r in
  let v = union b g in
  if mem x v then dfs r' g b else
  let v' = dfs (successors x) (add x g) b in
  assert {diff (add x v') b == add x (diff v' b) };
  let v'' = dfs r' g (add x v') in
  assert {diff v'' b == union (diff v'' (add x v')) (diff (add x v') b) };


[session]   [zip]

Generated by why3doc 0.88.3