Acyclicity test in graph

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

• vertices : this constant is the set of graph vertices
• successor : this function gives for each vertex the set of vertices directly joinable from it

The algorithm is depth-first-search in the graph. It picks randomly the son on which recursive call is done.
The acyclicity answers false if it finds a cycle, true otherwise
Fully automatic proof.

Notice the program uses MLW exceptions.

module TestAcyclicGraph
  use import int.Int
  use import list.List
  use import list.Append
  use import list.Mem as L
  use import list.HdTlNoOpt
  use import list.Elements as E
  use import init_graph.GraphSetSucc

predicate reachableplus (x y: vertex) =
  exists l. l <> Nil /\ path x l y

predicate accessplus_to (s: set vertex) (y: vertex) =
  forall x. mem x s -> reachableplus x y

predicate cycle (l: list vertex) =
  let x = hd l in  l <> Nil /\ path x l x 

type env = {blacks: set vertex; grays: set vertex}

predicate edges_in (s: set vertex) =
  forall x x'. mem x s -> edge x x' -> mem x' s

lemma paths_in :
  forall x l z s. edges_in s -> mem x s -> path x l z -> mem z s

predicate wf_env (e: env) =
  let {blacks = b; grays = g} = e in 
  subset g vertices /\ subset b vertices /\
  inter b g == empty /\ edges_in b 

predicate subenv (e e': env) =
  subset e.blacks e'.blacks /\ e.grays == e'.grays

predicate black_cycle (l: list vertex) (e: env) =
  cycle l /\ subset (elements l) e.blacks

let add_grays x e =
  returns {r -> r.blacks = e.blacks /\ r.grays = add x e.grays}
  {blacks = e.blacks; grays = add x e.grays}

let add_blacks x e =
  returns {r -> r.blacks = add x e.blacks /\ r.grays = remove x e.grays}
  {blacks = add x e.blacks; grays = remove x e.grays}

exception CycleAt vertex

let rec dfs r e =
requires {subset r vertices}
requires {forall x. mem x r -> accessplus_to e.grays x}
requires {wf_env e}
requires {forall l. not black_cycle l e}
returns {e' -> wf_env e' /\ subenv e e'}
returns {e' -> subset r e'.blacks}
returns {e' -> forall l. not black_cycle l e'}
raises { CycleAt x -> exists l. cycle (Cons x l) }
  if is_empty r then e
  else let x = choose r in let r' = remove x r in
  if mem x e.grays then raise (CycleAt x) else
  let e1 =
    if mem x e.blacks then e else
    dfs (successors x) (add_grays x e) in
  let ghost e2 = add_blacks x e1 in
  assert {forall l. not black_cycle l e1 -> black_cycle l e2 -> L.mem x l};
  dfs r' (add_blacks x e1)

let is_acyclic () =
ensures {result = forall l. not cycle l}
  try
    let e = dfs vertices {blacks = empty; grays = empty} in
    assert {e.blacks == vertices};
    assert {forall l. (black_cycle l e <-> cycle l)};
    true
  with CycleAt x -> false
  end

end