DFS in graph (array + lists)

The graph is represented by array (list of successors)

The algorithm is depth-first-search in the graph. It picks the first son in list of successors and makes recursive call with it.
The proof is mutually recursive on pre and post conditions. Fully automatic proof.


module GraphArraySucc
  use import int.Int
  use import array.Array
  use import list.List
  use import list.Mem
  use import list.NumOcc
  use import list.Append

  type graph = array (list int)
  predicate spl (lv: list int) = forall x: int. mem x lv -> num_occ x lv = 1

  function order (g: graph) : int = length g
  predicate vertex (g: graph) (x: int) = 0 <= x < order g
  predicate out (g: graph) (x: int)  = forall y: int. vertex g x -> mem y g[x] -> vertex g y
  predicate wf (g: graph) = forall x: int. vertex g x -> out g x
  predicate edge (x y: int) (g: graph) = vertex g x /\ mem y g[x]

  lemma mem_decidable:
    forall x: int, lv: list int. mem x lv \/ not mem x lv

  lemma spl_single:
    forall x: int. spl (Cons x Nil)

  lemma spl_expansion:
    forall x: int, l: list int. spl l -> not (mem x l) -> spl (l ++ (Cons x Nil))

  lemma spl_sub:
    forall lv lv1 lv2: list int. lv = lv1 ++ lv2 -> spl lv -> spl lv1 /\ spl lv2

end

module GraphArraySuccPath
  use import GraphArraySucc
  use import int.Int
  use import array.Array
  use import list.List
  use import list.Mem
  use import list.Append

  inductive path int (list int) int graph =
  | Path_empty:
      forall x: int, g: graph. vertex g x -> path x Nil x g
  | Path_cons:
      forall x y z: int, l: list int, g: graph.
      edge x y g -> path y l z g -> path x (Cons x l) z g

  predicate path_fst_not_twice (x z: int) (l: list int) (g: graph) =
    path x (Cons x l) z g /\ (not mem x l)

  lemma path_edge:
    forall x z: int, g: graph. path x (Cons x Nil) z g -> edge x z g

  lemma path_hd:
    forall x y z: int, l: list int, g: graph. path x (Cons y l) z g -> x = y

  lemma path_right_extension:
    forall x y z: int, l: list int, g: graph.
    wf g -> path x l y g -> edge y z g -> path x (l ++ Cons y Nil) z g

  lemma path_right_inversion:
    forall x z: int, l: list int, g: graph. path x l z g ->
       (x = z /\ l = Nil)
    \/ (exists y: int, l': list int.
        path x l' y g /\ edge y z g /\ l = l' ++ Cons y Nil)

  lemma path_trans:
    forall x y z: int, l1 l2: list int, g: graph.
    path x l1 y g -> path y l2 z g -> path x (l1 ++ l2) z g

  lemma empty_path:
    forall x z: int, g: graph. path x Nil z g -> x = z

  lemma path_decomposition:
    forall x y z: int, l1 l2: list int, g: graph.
    path x (l1 ++ Cons y l2) z g -> path x l1 y g /\ path y (Cons y l2) z g

  lemma path_vertex_l :
    forall x y z: int, l : list int, g : graph.
    wf g -> vertex g x -> path x l z g -> mem y l -> vertex g y

  lemma path_vertex_r :
    forall x z : int, l : list int, g : graph.
    wf g -> vertex g x -> path x l z g -> vertex g z

  lemma path_vertex_last_occ :
    forall x y z: int, l : list int, g: graph.
    path x l z g -> mem y l ->
    (exists l1 l2 : list int. l = l1 ++ (Cons y l2) /\ (path_fst_not_twice y z l2 g))
end

module Dfs

  use import int.Int
  use import ref.Ref
  use import array.Array
  use import set.Fset
  use import list.List
  use import list.Mem
  use import list.HdTlNoOpt
  use import list.NthNoOpt
  use import list.Append
  use import list.Reverse
  use import list.Elements as E
  use import GraphArraySucc
  use import GraphArraySuccPath

  type color = WHITE | GRAY | BLACK

  predicate nodeflip (x: int) (c1 c2: array color) =
    c1[x] = WHITE /\ c2[x] <> WHITE

  predicate whitepath (x: int) (l: list int) (z: int) (g: graph) (c: array color) =
   path x l z g /\ (forall y: int. mem y l -> c[y] = WHITE) /\ c[z] = WHITE

  predicate whiteaccess (lv: list int) (z: int) (g: graph) (c: array color) =
    exists x l. mem x lv /\ whitepath x l z g c

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

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

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

  predicate whitepath_fst_not_twice (x: int) (l: list int) (z: int) (g: graph) (c: array color) =
     whitepath x l z g c /\ path_fst_not_twice x l z g

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

  lemma whitepath_decomp:
    forall x l z y g c. whitepath x l z g c -> mem y l -> exists l': list int. whitepath y l' z g c

  lemma whitepath_mem_decomposition_r: 
    forall x l z y g c. wf g -> vertex g x -> whitepath x l z g c -> (mem y l \/ y = z) -> exists l': list int. whitepath y l' z g c
    
  lemma whitepath_whitepath_fst_not_twice: 
    forall x z l g c. whitepath x l z g c -> exists l'. whitepath_fst_not_twice x l' z g c

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

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

  lemma whitepath_cons_fst_not_twice_inversion:
    forall x z l g c. whitepath_fst_not_twice x (Cons x l) z g c -> x <> z ->
    (exists y. edge x y g /\ whitepath y l z g (set c x GRAY))

  lemma whitepath_fst_not_twice_inversion : 
    forall x z l g c. whitepath_fst_not_twice x l z g c -> x <> z -> 
    (exists y l'. edge x y g /\ whitepath y l' z g (set c x GRAY))
    
  predicate nodeflip_whitepath (roots: list int) (g: graph) (c1 c2: array color) =
    forall z. nodeflip z c1 c2 -> whiteaccess roots z g c1

  predicate whitepath_nodeflip (roots: list int) (g: graph) (c1 c2: array color) =
    forall x l z. mem x roots -> whitepath x l z g c1 -> nodeflip z c1 c2

  lemma whitepath_trans:
    forall x l1 y l2 z g c. whitepath x l1 y g c -> whitepath y l2 z g c -> whitepath x (l1 ++ l2) z g c

  lemma whitepath_Y:
    forall x l z y x' l' g c. whitepath x l z g c -> (mem y l \/ y = z) -> whitepath x' l' y g c -> exists l0. whitepath x' l0 z g c

  predicate white_monotony (g: graph) (c1 c2: array color) =
    forall x: int. vertex g x -> c2[x] = WHITE -> c1[x] = WHITE

  predicate whitepath_monotony (g: graph) (c1 c2: array color) =
    forall x z: int, l: list int. vertex g x -> whitepath x l z g c2 -> whitepath x l z g c1

  predicate whitepath_cons (x: int) (g: graph) (c1 c2: array color) =
    forall y z: int, l: list int. mem y g[x] ->
    whitepath y l z g c2 -> whitepath x (Cons x l) z g c1
    

program


let rec dfs (g: graph) (x: int) (c: array color) =
  requires {wf g /\ vertex g x /\ Array.length c = order g}
  requires {c[x] = WHITE}
  ensures {white_monotony g (old c) c} 
  ensures {whitepath_nodeflip (Cons x Nil) g (old c) c}
  ensures {nodeflip_whitepath (Cons x Nil) g (old c) c}

'L0:
      c[x] <- GRAY;
      assert {whitepath_cons x g (at c 'L0) c};  (* nodeflip_whitepath *)
'L:
      let sons = ref (g[x]) in
      let ghost lv = ref Nil in
         while  ( !sons <> Nil) do
         invariant {(reverse !lv) ++ !sons = g[x]}
	 invariant {forall y. mem y !sons -> vertex g y}
         invariant {white_monotony g (at c 'L) c}
	 invariant {whitepath_monotony g (at c 'L) c}
         invariant {whitepath_nodeflip !lv g (at c 'L) c}
	 invariant {nodeflip_whitepath !lv g (at c 'L) c}

'L1:
         match !sons with
           | Nil -> ()
           | Cons y sons' ->
	       (*--------- whitepath_nodeflip ------------*)
	       assert {forall l z. whitepath y l z g (at c 'L) -> not whitepath y l z g c -> exists z'. (mem z' l \/ z' = z) /\ nodeflip z' (at c 'L) c};  
               assert {forall l z. whitepath y l z g (at c 'L) -> not whitepath y l z g c -> exists y' l' z'. (mem z' l \/ z' = z) /\ mem y' !lv /\ whitepath y' l' z' g (at c 'L)}; 
               assert {forall l z. whitepath y l z g (at c 'L) -> not whitepath y l z g c -> exists y' l'. mem y' !lv /\ whitepath y' l' z g (at c 'L)}; 
	       assert {forall l z. whitepath y l z g (at c 'L) -> not whitepath y l z g c -> nodeflip z (at c 'L) c};
               if c[y] = WHITE then begin
                  dfs g y c;
               end;
                  sons := sons';
                  lv := Cons y !lv
         end
         done;
'L2:
(*------- nodeflip_whitepath -----------*)
      assert {whitepath x Nil x g (at c 'L0)};
      assert {nodeflip_whitepath (Cons x Nil) g (at c 'L0) (at c 'L)};
      assert {forall z. nodeflip z (at c 'L) c -> exists l. whitepath x l z g (at c 'L0)};
      assert {forall z. nodeflip z (at c 'L0) c -> exists l. whitepath x l z g (at c 'L0)};
(*------- whitepath_nodeflip -----------*)
      assert {forall z l. whitepath x l z g (at c 'L0) -> x <> z -> nodeflip z (at c 'L0) c};
      assert {nodeflip x (at c 'L0) c};
      
      c[x] <- BLACK;
      assert {forall z. nodeflip z (at c 'L0) c <-> nodeflip z (at c 'L0) (at c 'L2)}

let dfs_main (g: graph) =
   requires { wf g }
   let n = length (g) in
   let c = make n WHITE in
   for i = 0 to n - 1 do
     if c[i] = WHITE then
       dfs g i c
   done

end

Generated by why3doc 0.86.1