```(* no edges from Black to White vertices
for dfs, i.e. no right-to-left edge in
spanning trees *)

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 noB2Wedge (g: graph) (c: array color) =
forall x y: int. vertex g x -> vertex g y -> c[x] = BLACK -> c[y] = WHITE -> 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{ noB2Wedge g c }
ensures { (old c)[x] = WHITE -> c[x] <> WHITE }
ensures { white_monotony g (old c) c }
ensures { noB2Wedge 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 { noB2Wedge 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 { noB2Wedge g c }
if c[x] = WHITE then
dfs g x c
done

end
```

Generated by why3doc 0.85