why3doc index index

DFS in graph - completeness of the whitepath theorem

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

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.
Every vertex reachable by a white path (w.r.t the old visited set) is in the result
Fully automatic proof, with inductive definition of white paths.

Notice that this proof does not use paths.

module DfsWhitePathCompleteness
  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 whiteaccess (r s v: set vertex) =
    forall z. mem z s -> exists x l. mem x r /\ wpath x l z v

  predicate nbtw (r v: set vertex) =
    forall x x'. edge x x' -> mem x r -> mem x' (union r 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
  variant {(cardinal vertices - cardinal v), (cardinal r)} =
  requires {subset r vertices }
  requires {subset v vertices }
  ensures {subset result vertices }
  ensures {subset v result }
  ensures {subset r result }
  ensures {nbtw (diff result v) result &&
           forall s. whiteaccess r s v -> subset s (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 dfs r' v else
  let v' = dfs (successors x) (add x v) in
  assert {diff v' v == add x (diff v' (add x v)) };
  let v'' = dfs r' v' in
  assert {diff v'' v == union (diff v'' v') (diff v' v) };


[session]   [zip]

Generated by why3doc 0.88.3