DFS in graph - soundness of the whitepath theorem

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

• vertices : this constant is the set of graph vertices
• successor : this function gives for each vertex the set of vertices directly joinable from it

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.
Quasi automatic proof, with inductive definition of white paths, mutable set of visited vertices, black/white color. The proof is similar to the functional one. One loop invariant is proved in Coq.

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.Length
  use import list.HdTlNoOpt
  use import list.Reverse
  use import list.Elements as E
  use import array.Array
  use import ref.Ref
  use import init_graph.GraphListArraySucc

  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_var:
    forall r r' b v. subset r r' -> whiteaccess r b v -> whiteaccess r' b v

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

  lemma wpath_covar2:
    forall x l z v v'. subset v v' -> wpath x l z v' -> wpath x l z v

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

  lemma wpath_trans:
    forall x l y l' z v. wpath x l y v -> wpath y l' z v -> wpath x (l ++ l') z v

  lemma whiteaccess_trans: 
    forall r r' b v. whiteaccess r r' v -> whiteaccess r' b v -> whiteaccess r b v

  lemma whiteaccess_cons:
    forall x s v. mem x vertices ->
      white_vertex x v -> whiteaccess (elements (successors x)) s v -> whiteaccess (add x empty) s v

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

  lemma path_wpathempty:
    forall y l z. wpath y l z empty -> path y l z

  lemma diff_inc:
    forall a b c: set 'alpha. subset c b -> subset b a -> diff a c = union (diff a b) (diff b c)
      by diff a c == union (diff a b) (diff b c)

  type color = WHITE | GRAY | BLACK

function non_white_set (array color): set vertex

axiom set_non_white:
  forall col x. mem x (non_white_set col) <-> mem x vertices /\ col[x] <> WHITE

let rec dfs1 x col (graph: array (list vertex)) (ghost v) =
  requires {Array.length graph = cardinal vertices /\ forall x. graph[x] = successors x}
  requires {Array.length col = cardinal vertices}
  requires {mem x vertices /\ col[x] = WHITE}
  requires {forall x. mem x !v <-> mem x vertices /\ col[x] <> WHITE}
  ensures {forall x. mem x !v <-> mem x vertices /\ col[x] <> WHITE}
  ensures {subset !(old v) !v }
  ensures {whiteaccess (add x empty) (diff !v !(old v)) !(old v) }
  ensures {forall x. mem x vertices -> col[x] = GRAY <-> (old col)[x] = GRAY}
'L0:
  let ghost v0 = !v in
  let ghost col0 = Array.copy col in
  assert {not mem x v0};
  col[x] <- GRAY; v := add x !v; 
  let sons = ref graph[x] in
  let ghost dejavu = ref Nil in
  while !sons <> Nil do
    invariant {subset (elements !sons) vertices}
    invariant {subset !v vertices}
    invariant {forall z. mem z vertices -> (col[z] = GRAY <-> col0[x<-GRAY][z] = GRAY) }
    invariant {forall z. mem z !v <-> mem z vertices /\ col[z] <> WHITE}
    invariant {whiteaccess (elements !dejavu) (diff !v (add x v0)) v0}
    invariant {subset (add x v0) !v}
    invariant {successors x = (reverse !dejavu) ++ !sons}
    let y = hd !sons in
      if col[y] = WHITE then dfs1 y col graph v;
    sons := tl !sons;
    dejavu := Cons y !dejavu;
  done;
'L1:
  let ghost v' = !v in
  assert {whiteaccess (add x empty) (diff v' (add x v0)) v0
    by whiteaccess (elements (successors x)) (diff v' (add x v0)) v0 };
  assert {wpath x Nil x v0};
  assert {whiteaccess (add x empty) (diff v' v0) v0
    by diff v' v0 == add x (diff v' (add x v0))
    by mem x v'};
  col[x] <- BLACK
    
let dfs_main graph =
  requires {Array.length graph = cardinal vertices}
  requires {forall x. graph[x] = successors x}
  ensures {let s = non_white_set result in
    whiteaccess vertices s empty
    so  forall z. mem z s -> exists y l. mem y vertices /\ path y l z }
  let col = make (cardinal vertices) WHITE in
  let ghost v = ref empty in 
  let ghost dejavu = ref Nil in
  for x = 0 to (cardinal vertices) - 1  do
    invariant {subset !v vertices}
    invariant {forall z. mem z !v <-> mem z vertices /\ col[z] <> WHITE}
    invariant {whiteaccess (elements !dejavu) !v empty}
    invariant {forall y. mem y (elements !dejavu) <-> 0 <= y < x}
    if col[x] = WHITE then dfs1 x col graph v;
    dejavu := Cons x !dejavu;
  done;
  col

(* let rec dfs1 x col graph =
  col[x] <- GRAY; 
  let sons = ref graph[x] in
  while !sons <> Nil do
    let y = hd !sons in
      if col[y] = WHITE then dfs1 y col;
    sons := tl !sons;
  done;
  col[x] <- BLACK
    
let dfs_main graph =
  let col = make (cardinal vertices) WHITE in
  for x = 0 to (cardinal vertices) - 1  do
    if col[x] = WHITE then dfs1 x col;
  done;
  col
*) 

end