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 makes simple depth-first-search in the graph, looking for a loop-back to a gray node.
Fully automatic proof.

```
module DagTest
use import int.Int
use import int.MinMax
use import list.List
use import list.Length
use import list.Append
use import list.Mem as L
use import list.NumOcc
use import list.Elements as E
use import list.HdTlNoOpt
use import init_graph.GraphSetSucc
use import map.Map
use import ref.Ref
use import ref.Refint

predicate lmem (x: 'a) (s: list 'a) = L.mem x s

```

Ranks and Lists

```
(* simple lists *)

predicate simplelist (l: list 'a) = forall x. num_occ x l <= 1

```

Sets

```
lemma inter_assoc:
forall s1 s2: set 'a. inter s1 s2 == inter s2 s1

lemma inter_add:
forall s1 s2: set 'a, x: 'a. not mem x s2 -> inter (add x s1) s2 == inter s1 s2

lemma inter_subset_inter:
forall s1 s2 s3: set 'a. inter s1 s2 = empty -> subset s3 s2 -> inter s1 s3 = empty

lemma subset_add:
forall x: 'a, s s': set 'a. subset s' (add x s) -> mem x s' \/ subset s' s

```

Predicates definitions

```
predicate no_black_to_white (blacks grays: set vertex) =
forall x x'. edge x x' -> mem x blacks -> mem x' (union blacks grays)

predicate no_black_to_gray (blacks grays: set vertex) =
forall x x'. edge x x' -> mem x blacks -> not mem x' grays

predicate circle (x: vertex) (l: list vertex) =
l <> Nil /\ simplelist l /\ path x l x

predicate black_circle (x: vertex) (l: list vertex) (b: set vertex) =
circle x l /\ subset (elements l) b

predicate reachable (x z: vertex) =
exists l. path x l z

predicate access_to (s: set vertex) (y: vertex) =
forall x. mem x s -> reachable x y

```

Specialized lemmas

```
use import list.Permut

lemma circle_rotate:
forall x y l1 l2. circle x (Cons x (l1 ++ Cons y l2)) -> circle y (Cons y (l2 ++ Cons x l1))

let lemma circle_rotate_to (x y: vertex) (l: list vertex)
requires {circle x l}
requires {lmem y l}
ensures {exists l'. circle y l' /\ permut l l'}
= if y = x then () else
assert {exists l1 l2. l = Cons x l1 ++ Cons y l2}; ()

```

dfs1

```
predicate wff_color (blacks grays: set vertex) =
no_black_to_white blacks grays /\ no_black_to_gray blacks grays /\ inter blacks grays = empty

use import list.Reverse

predicate gray_chain_edge (s: list vertex) (x: vertex) =
s <> Nil -> edge (hd s) x /\ path (hd (reverse s)) (reverse s) x /\ simplelist s

lemma simple_list_decomp:
forall l1 l2: list 'a. simplelist (l1 ++ l2) -> simplelist l1 /\ simplelist l2

lemma simple_non_empty_path_decomp_general:
forall x l z y. path x l z -> simplelist l -> lmem y l -> exists l'. path y l' z /\ simplelist l' /\ l' <> Nil

let rec dfs1 x blacks grays (ghost stack) =
requires {mem x vertices}
requires {grays == elements stack}
requires {gray_chain_edge stack x}
requires {not mem x (union blacks grays)}
(* invariants *)
requires {wff_color blacks grays}
requires {forall x l. not black_circle x l blacks}
returns {(r, b) -> r -> wff_color b grays}
returns {(r, b) -> r -> forall x l. not black_circle x l b}
returns {(r, _) -> not r -> exists x l. circle x l}
(* post-conditions *)
returns {(_, b) -> mem x b}
(* monotony *)
returns {(_, b) -> subset blacks b}

let (r1, b1) =
dfs' (successors x) blacks (add x grays) (Cons x stack) in
assert {forall y l. black_circle y l (add x b1) -> lmem x l -> exists l'. black_circle x l' (add x b1)};
assert {forall l. black_circle x l (add x b1) -> exists y. edge y x /\ mem y (add x b1)};
(r1, add x b1)

```

dfs'

```
with dfs' roots blacks grays (ghost stack) =
requires {subset roots vertices}
requires {grays == elements stack}
requires {forall x. mem x roots -> gray_chain_edge stack x}
(* invariants *)
requires {wff_color blacks grays}
requires {forall x l. not black_circle x l blacks}
returns {(r, b) -> r -> wff_color b grays}
returns {(r, b) -> r -> forall x l. not black_circle x l b}
returns {(r, _) -> r = false -> exists x l. circle x l}
(* post-conditions *)
returns {(r, b) -> r -> subset roots b}
(* monotony *)
returns {(_, b) -> subset blacks b}

if is_empty roots then (true, blacks)
else
let y = choose roots in
let roots' = remove y roots in
if mem y grays then (false, blacks)
else
let (r3, b3) =
if mem y blacks then (true, blacks)
else dfs1 y blacks grays stack in
if r3 then dfs' roots' b3 grays stack
else (false, b3)

let dag_main () =
returns {(r, _) -> r = not exists x l. circle x l /\ subset (elements l) vertices}
dfs' vertices empty empty Nil

```

[all proof is here (zip file)]

```
end
```

Generated by why3doc 0.87.0