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 DfsWhitePathGraySoundness
  use import int.Int
  use import list.List
  use import list.Append
  use import list.Mem as L
  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 circle (x: vertex) (l: list vertex) =
  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_circle (x: vertex) (l: list vertex) (e: env) =
  circle x 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 NotDagAt 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 x l. not black_circle x l e}
returns {(_, e') -> wf_env e' /\ subenv e e'}
returns {(_, e') -> subset r e'.blacks}
returns {(v, e') -> forall x l. not black_circle x l e'}
raises { NotDagAt x -> exists l. circle x l }
  if is_empty r then (true, e)
  else let x = choose r in let r' = remove x r in
  if mem x e.grays then raise (NotDagAt x) else
  let (_, e1) =
    if mem x e.blacks then (true, e) else
    dfs (successors x) (add_grays x e) in
  let ghost e3 = add_blacks x e1 in
  assert {forall y l. not black_circle y l e1 -> black_circle y l e3 -> L.mem x l};
  let (v2, e2) = dfs r' (add_blacks x e1) in
  (v2, e2)

let is_acyclic () =
ensures {result = forall x l. not circle x l}
  try
    let (_, e) = dfs vertices {blacks = empty; grays = empty} in
    assert {forall x l. black_circle x l e <-> circle x l
            by e.blacks == vertices};
    true
  with NotDagAt x -> false
  end

end