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.Reverse
  use import list.Elements as E
  use import array.Array
  use import ref.Ref
  use import init_graph.GraphListArraySucc

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

type color = WHITE | GRAY | BLACK
exception CycleAt vertex

predicate env_is_col (e: env) (col: array color) =
  (forall x. mem x e.blacks <-> mem x vertices /\ col[x] = BLACK)
  /\ (forall x. mem x e.grays <-> mem x vertices /\ col[x] = GRAY)

let rec dfs1 x (ghost e) col =
  requires {mem x vertices /\ col[x] = WHITE }
  requires {col[x] = WHITE /\ Array.length col = cardinal vertices}
  requires {env_is_col !e col /\ wf_env !e}
  requires {accessplus_to !e.grays x}
  requires {forall l. not black_cycle l !e}
  ensures {mem x !e.blacks}
  ensures {env_is_col !e col /\ wf_env !e /\ subenv !(old e) !e}
  ensures {forall l. not black_cycle l !e}
  raises { CycleAt x -> exists l. cycle (Cons x l) }
  
'L0:
  let ghost e0 = {blacks = !e.blacks; grays = add x !e.grays} in
  col[x] <- GRAY; e := {blacks = !e.blacks; grays = add x !e.grays};
  let sons = ref (successors x) in
  let ghost dejavu = ref Nil in
  while !sons <> Nil do
    invariant {subset (elements !sons) (elements (successors x))}
    invariant {successors x = (reverse !dejavu) ++ !sons} 
    invariant {env_is_col !e col /\ wf_env !e /\ subenv e0 !e}
    invariant {forall y. L.mem y !sons -> accessplus_to !e.grays y}
    invariant {subset (elements !dejavu) !e.blacks} 
    invariant {forall l. not black_cycle l !e}
    let y = hd !sons in
      if col[y] = GRAY then begin assert {mem y !e.grays};
        raise (CycleAt x) end else
      if col[y] = WHITE then dfs1 y e col;
    sons := tl !sons;
    dejavu := Cons y !dejavu;
  done;
'L1:
  let ghost e1 = !e in
  col[x] <- BLACK;
  e := {blacks = add x !e.blacks; grays = remove x !e.grays};
  assert {forall l. not black_cycle l e1 -> black_cycle l !e -> L.mem x l}

let is_acyclic () =
ensures {result = forall l. not cycle l}
  try
    let col = make (cardinal vertices) WHITE in
    let ghost e = ref {blacks = empty; grays = empty} in
    let ghost e0 = !e in 
    for x = 0 to (cardinal vertices) - 1  do
      invariant {forall y. 0 <= y < x -> col[y] = BLACK}
      invariant {env_is_col !e col /\ wf_env !e /\ subenv e0 !e}
      invariant {forall l. not black_cycle l !e}
      if col[x] = WHITE then dfs1 x e col
    done;
    assert {!e.blacks == vertices};
    assert {forall l. (black_cycle l !e <-> cycle l)};
    true
  with CycleAt x -> false
  end

(* let rec dfs1 x col =
  col[x] <- GRAY; 
  let sons = ref (successors x) in
  while !sons <> Nil do
    let y = hd !sons in
      if col[y] = GRAY then raise (CycleAt x) else
      if col[y] = WHITE then dfs1 y col;
    sons := tl !sons;
  done

let is_acyclic () =
  try
    for x = 0 to (cardinal vertices) - 1  do
      if col[x] = WHITE then dfs1 x col
    done;
    true
  with CycleAt x -> false
  end
*)

 end