why3doc index index



DFS in graph - 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 non inductive definition of white paths.

Notice that this proof uses paths.


module DfsWhitePathSoundness
  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)
 
  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

  lemma whitepath_id:
    forall x v. not mem x v -> whitepath x Nil x v

  lemma whitepath_sub:
    forall v v' x l y. subset v v' -> whitepath x l y v' -> whitepath x l y v

  lemma whitepath_cons:
    forall x x' y l v. not mem x v -> edge x x' -> whitepath x' l y v -> whitepath x (Cons x l) y v

program


let rec dfs r v
  variant {(cardinal vertices - cardinal v), (cardinal r)} =
  requires {subset r vertices }
  requires {subset v vertices }
  ensures {subset v result}
  ensures {subset result vertices}
  ensures {forall z. mem z (diff result v) -> exists y l. mem y r /\ whitepath y l 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 dfs r' v else
  let v' = dfs (successors x) (add x v) in
  let v'' = dfs r' v' in
  (*-------- nodeflip_whitepath ------------------*)
  assert {forall z. mem z (diff v'' v) -> z <> x ->
     (exists y l. (mem y r'/\ whitepath y l z v' ))
  \/ (exists y' l'. mem y' (successors x) /\ whitepath y' l' z v
     so exists l. whitepath x l z v)};
  v''

let dfs_main roots =
  requires {subset roots vertices}
  ensures {forall z. mem z result -> exists y l. mem y roots /\ path y l z}
  dfs roots empty

end

[session]   [zip]



Generated by why3doc 0.88.3