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.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

```

### program

```

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

```

```
```

```
```

#### extracted program

```
(* 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

```

Generated by why3doc 0.88.3