Iterative breadth search with queue (soundness)

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 queue.Queue
  use import list.NumOcc
  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 (q: Queue.t vertex) (s: set vertex) 
  variant { cardinal s } =
  ensures {union (elements (old q.elts)) s == elements q.elts }
  if not is_empty s then begin
    let x = choose s in
    Queue.push x q;
    push_set q (remove x s)
  end

let rec bfs 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 Queue.is_empty r then v else
   let x = Queue.pop r in
'L1:
   if mem x v then bfs r v else begin
     push_set r (successors x);
   let v' = bfs 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 bfs_main (roots: Queue.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}
   bfs roots empty

end