nwtb in dfs for undirected graphs

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

• g : an array of lists of successors for each node
• g[x] : is the list of vertices directly joinable from x

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

 type graph = array (list int)
 predicate edge int int

 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 g_edge (g: graph) (x: int) = forall y : int. (vertex g x /\ mem y g[x]) <-> edge x y
 predicate simple (g: graph) (x: int) = forall y: int. vertex g x -> mem y g[x] -> num_occ y g[x] = 1
 predicate double (g: graph) (x: int) = forall y: int. vertex g x -> mem y g[x] -> mem x g[y]
 predicate wf (g: graph) = forall x: int. vertex g x -> out g x /\ g_edge g x /\ (* simple g x /\ *) double g x

end

module NoWhiteToBlackUGraph

 use import int.Int
 use import ref.Ref
 use import array.Array
 use import list.List
 use import list.NumOcc
 use import list.Mem
 use import GraphArraySucc

type color = WHITE | GRAY | BLACK

predicate noW2Bedge (g: graph) (c: array color) =
   forall x y: int. vertex g x -> vertex g y -> c[x] = WHITE -> c[y] = BLACK -> not mem y g[x]

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

let rec dfs (g: graph) (x: int) (c: array color) =
  requires{ wf g /\ vertex g x /\ length c = order g }
  requires{ noW2Bedge g c }
  ensures { (old c)[x] = WHITE -> c[x] <> WHITE }
  ensures { white_monotony g (old c) c }
  ensures { noW2Bedge g c }
'L:
  c[x] <- GRAY;
  let sons = ref (g[x]) in
  while !sons <> Nil do
    invariant { white_monotony g (at c 'L) c }
    invariant { forall y: int. mem y !sons -> edge x y }
    invariant { forall y: int. edge x y -> c[y] = WHITE -> mem y !sons }
    invariant { noW2Bedge g c }
    match !sons with
    | Nil -> ()
    | Cons y sons' ->
      if c[y] = WHITE then dfs g y c;
      sons := sons'
     end;
    done;
    c[x] <- BLACK

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

end