Iterative depth first search with stack

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 a iterative depth-first-search with a stack. The proof is quasi similar to random search.
This soundness proof is fully automatic.

module Dfs_stack
  use import int.Int
  use import ref.Ref
  use import list.List
  use import list.Length
  use import list.Mem as L
  use import list.Elements as E
  use import list.Append
  use import stack.Stack
  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_covar:
    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

let rec push_set (p: Stack.t vertex) (s: set vertex) 
  variant { cardinal s } =
  ensures { union (elements (old p.elts)) s == elements p.elts }
  if not is_empty s then begin
    let x = choose s in
    Stack.push x p;
    push_set p (remove x s)
  end

let rec dfs r v
  variant {(cardinal vertices - cardinal v), L.length (r.elts)} = 
  requires {subset (elements r.elts) vertices }
  requires {subset v vertices }
  ensures {subset v result }
  ensures {subset result vertices }
  raises {Empty}
  ensures {subset v result}
  ensures {forall z. mem z (diff result v) -> exists y l. L.mem y (old r).elts /\ whitepath y l z v}

   if Stack.is_empty r then v else
   let x = Stack.pop r in
'L1:
   if mem x v then dfs r v else begin
     push_set r (successors x);
   let v' = dfs r (add x v) in
   assert {forall z. mem z (diff v' v) -> z <> x ->
      (exists y l. mem y (elements (at r 'L1).elts) /\ (whitepath y l z v by whitepath y l z (add x v)))
   \/ ((exists l. whitepath x l z v)
       by  exists x' l'. edge x x' /\ whitepath x' l' z v)};
          v'
      end

let dfs_main (roots: Stack.t vertex) =
   requires {subset (elements (roots.elts)) vertices}
   raises {Empty}
   ensures {forall z. mem z result -> exists y l. L.mem y (old roots).elts /\ path y l z}
   dfs roots empty

end