Iterative depth first search with stack

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

The algorithm is a ministep of a random search in the graph. It is generic to any search strategy.
The proof is adapted from Dowek and Munoz and 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
  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 (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 (roots: Stack.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 Stack.is_empty roots then
     visited
   else
     let x = Stack.pop roots in
'L1:
      if mem x visited then
      	 dfs roots visited
      else begin
         push_set roots (successors x);
'L2:
     	 let r = dfs 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 dfs_main (roots: Stack.t vertex) =
   requires {subset (elements (roots.elts)) vertices}
   raises {Empty}
   dfs roots empty

end

Generated by why3doc 0.86.1