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

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.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 path_wpathempty:
    forall y l z. wpath y l z empty -> path y l z

  type color = WHITE | BLACK

let rec dfs r (ghost v) col =
  requires {subset (elements r) vertices }
  requires {subset !v vertices }
  requires {Array.length col = cardinal vertices}
  requires {forall x. mem x !v <-> mem x vertices /\ col[x] = BLACK}
  ensures {subset !(old v) !v }
  ensures {subset !v vertices }
  ensures {forall x. mem x !v <-> mem x vertices /\ col[x] = BLACK}
  ensures {whiteaccess (elements r) (diff !v !(old v)) !(old v) }
'L0:
  let ghost v0 = !v in
  match r with
  | Nil -> ()
  | Cons x r' ->  if col[x] = BLACK then dfs r' v col else begin
    v := add x !v; col[x] <- BLACK;
    dfs (successors x) v col;
'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
      by subset (diff v' (add x v0)) (diff v' v0)
      by subset v0 (add x 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)) };
    dfs r' v col;
'L2:
    let ghost v'' = !v in
    assert {diff v'' v0 == union (diff v'' v') (diff v' v0) };
    assert {whiteaccess (elements r') (diff v'' v') v0
      by subset v0 v' }
    end
  end

let dfs_main roots =
  requires {subset (elements roots) vertices}
  ensures {whiteaccess (elements roots) (elements result) empty
   so  forall z. mem z (elements result) -> exists y l. mem y (elements roots) /\ path y l z }
  let ghost v = ref empty in let col = make (cardinal vertices) WHITE in
  dfs roots v col;
  let res = ref Nil in
  for x = 0 to (cardinal vertices) - 1  do
    invariant {forall y. L.mem y !res <-> 0 <= y < x /\ col[y] = BLACK}
    if col[x] = BLACK then res := Cons x !res
  done;
  !res

(* let rec dfs' r col =
  match r with
  | Nil -> ()
  | Cons x r' ->  if col[x] = BLACK then dfs' r' col else begin
    col[x] <- BLACK;
    dfs' (successors x) col;
    dfs' r' col;
    end
  end

let dfs_main' roots =
  let col = make (cardinal vertices) WHITE in
  dfs' roots col;
  let res = ref Nil in
  for x = 0 to (cardinal vertices) - 1  do
    if col[x] = BLACK then res := Cons x !res
  done;
  !res
*)

end