Breadth first search in graph

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

The algorithm is standard bfs in graph. It is derived from generic random ministep search.
The proof is adapted from Dowek and Munoz and is fully automatic.


module Bfs
  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 init_graph.GraphSetSucc
  use import init_graph.GraphSetSuccPath

 predicate white_vertex (x: vertex) (v: set vertex) =
    not (mem x v)
 
  predicate nodeflip (x: vertex) (v1 v2: set vertex) =
    white_vertex x v1 /\ not (white_vertex x v2)

  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

  predicate whiteaccess (r: set vertex) (z: vertex) (v: set vertex) =
    exists x l. mem x r /\ whitepath x l z v

  predicate path_fst_not_twice (x: vertex) (l: list vertex) (z: vertex) = 
    path x l z /\ 
    match l with
    | Nil -> true
    | Cons _ l' -> x <> z /\ not (L.mem x l')
    end

 lemma path_suffix_fst_not_twice:
    forall x z l "induction". path x l z -> 
      exists l1 l2. l = l1 ++ l2 /\ path_fst_not_twice x l2 z

  lemma path_path_fst_not_twice:
    forall x z l. path x l z -> 
      exists l'. path_fst_not_twice x l' z /\ subset (E.elements l') (E.elements l)

  predicate whitepath_fst_not_twice (x: vertex) (l: list vertex) (z: vertex) (v: set vertex) =
     whitepath x l z v /\ path_fst_not_twice x l z

  lemma whitepath_decomposition: 
    forall x l1 l2 z y v. whitepath x (l1 ++ (Cons y l2)) z v -> whitepath x l1 y v /\ whitepath y (Cons y l2) z v

  lemma whitepath_mem_decomposition_r: 
    forall x l z y v. whitepath x l z v -> L.mem y (l ++ (Cons z Nil)) -> exists l': list vertex. whitepath y l' z v
    
  lemma whitepath_whitepath_fst_not_twice: 
    forall x z l v. whitepath x l z v -> exists l'. whitepath_fst_not_twice x l' z v

  lemma path_cons_inversion:
    forall x z l. path x (Cons x l) z -> exists y. edge x y /\ path y l z

  lemma whitepath_cons_inversion:
    forall x z l v. whitepath x (Cons x l) z v -> exists y. edge x y /\ whitepath y l z v

  lemma whitepath_cons_fst_not_twice_inversion:
    forall x z l v. whitepath_fst_not_twice x (Cons x l) z v -> x <> z ->
    (exists y. edge x y /\ whitepath y l z (add x v))

  lemma whitepath_fst_not_twice_inversion : 
    forall x z l v. whitepath_fst_not_twice x l z v -> x <> z -> 
    (exists y l'. edge x y /\ whitepath y l' z (add x v))
    
  predicate nodeflip_whitepath (roots v1 v2: set vertex) =
    forall z. nodeflip z v1 v2 -> whiteaccess roots z v1

  predicate whitepath_nodeflip (roots v1 v2: set vertex) =
    forall x l z. mem x roots -> whitepath x l z v1 -> nodeflip z v1 v2


program


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 (roots: Queue.t vertex) (visited: set vertex): set vertex 
  variant {(cardinal vertices - cardinal visited), L.length (roots.elts)} = 
  requires {subset (elements (roots.elts)) vertices }
  requires {subset visited vertices }
  raises {Empty}
  ensures {subset visited result}
  ensures {whitepath_nodeflip (elements (old roots.elts)) visited result}
  ensures {nodeflip_whitepath (elements (old roots.elts)) visited result}
'L0:
   if Queue.is_empty roots then
     visited
   else
     let x = Queue.pop roots in
'L1:
      if mem x visited then
      	 bfs roots visited
      else begin
         push_set roots (successors x);
'L2:
     	 let r = bfs roots (add x visited) in
          (*----------- nodeflip_whitepath -----------*)
          assert {forall z. nodeflip z visited r -> z = x \/ nodeflip z (add x visited) r };
          (* case 1-1: nodeflip z visited r /\ z = x *)
             assert {whitepath x Nil x visited};
          (* case 1-2: nodeflip z visited r /\ z <> x *)
             assert {let roots' = elements (at roots.elts 'L1) in
                     forall z. nodeflip z (add x visited) r -> whiteaccess roots' z (add x visited) 
                     \/ whiteaccess (successors x) z (add x visited)};
	     assert {forall x' l z. whitepath x' l z (add x visited) -> whitepath x' l z visited};
             assert {forall z x' l. edge x x' -> whitepath x' l z visited -> whitepath x (Cons x l) z visited};
             assert {subset (elements (at roots.elts 'L1))(elements (at roots.elts 'L0))};
             assert {subset (elements (at roots.elts 'L2))(union (elements (at roots.elts 'L1)) (successors x))};
             assert {forall z. nodeflip z (add x visited) r -> whiteaccess (elements (at roots.elts 'L0)) z visited};

	  (*-------------- whitepath_nodeflip -------------*)

	  (* case 1: whitepath x l z visited /\ x = z *)
            assert {mem x r};
	  
	  (* case 2: whitepath x l z /\ x <> z *)
            (* using lemma whitepath_whitepath_fst_not_twice *)
            assert {forall l z. whitepath x l z visited -> x <> z 
               -> exists x' l'. edge x x' /\ whitepath x' l' z (add x visited)};  
               (* same as lemma whitepath_inversion *)
            assert {forall l z. whitepath x l z visited -> x <> z -> nodeflip z (add x visited) r}; 
	  assert {forall l z. whitepath x l z visited -> nodeflip z visited r};  
	  
	  (* case 3: whitepath roots' l z *)
            (* case 3-1: whitepath roots' l z /\ L.mem x l *)
              assert {forall y l z. whitepath y l z visited -> (L.mem x l \/ x = z)
                 -> exists l'. whitepath x l' z visited};
              (* goto cases 1-2 *)
            (* case 3-2: whitepath roots' l z /\ not (L.mem x l) *)
              assert {let roots' = elements (at roots.elts 'L1) in
                 forall y l z. mem y roots' -> whitepath y l z visited -> not (L.mem x l \/ x = z)
                 -> whitepath y l z (add x visited)};  
          r
      end

let bfs_main (roots: Queue.t vertex) =
   requires {subset (elements (roots.elts)) vertices}
   raises {Empty}
   bfs roots empty

end

Generated by why3doc 0.86.1