why3doc index index

# 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

```

### program

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

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};

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

```

```