why3doc index index

# Tarjan 1972, Articulation Points in Undirected Graph

The graph is represented by a pair (`vertices`, `successor`)

• `vertices` : this constant is the set of graph vertices
• `successors` : this function gives for each vertex the set of vertices directly joinable from it
The algorithm makes depth-first-search in the graph. After stacking the vertices in the (pre-)order of their visit, one finds the strongly connected components.
Fully automatic proof except 2 assertions proved in Coq.

```

module ArtTarjan72
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 init_graph.GraphSetSucc
use import map.Map
use import map.Const

predicate lmem (x: 'a) (s: list 'a) = L.mem x s
function infty (): int = cardinal vertices

lemma lmem_dec:
forall x: 'a, l: list 'a. lmem x l \/ not lmem x l

```

#### Sets

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

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

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

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

forall x: 'a, s1 s2: set 'a. mem x s2 -> diff (add x s1) s2 == diff s1 s2

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

forall x: 'a, s s': set 'a. union (add x s) s' == add x (union s s')

forall x: 'a, s s': set 'a. union s (add x s') == add x (union s s')

lemma union_com:
forall s s': set 'a. union s s' == union s' s

lemma union_var_l:
forall s s' t: set 'a. subset s s' -> subset (union s t) (union s' t)

lemma union_var_r:
forall s t t': set 'a. subset t t' -> subset (union s t) (union s t')

(* sets of sets *)

function set_of (set (set 'a)): set 'a

axiom set_of_empty:
set_of empty = (empty : set 'a)

forall s: set 'a, sx. set_of (add s sx) == union s (set_of sx)

predicate one_in_set_of (sccs: set (set 'a)) =
forall x. mem x (set_of sccs) -> exists cc. mem x cc /\ mem cc sccs

clone set.FsetInduction with type t = set vertex, predicate p = one_in_set_of

lemma set_of_elt:
forall sccs: set (set vertex). one_in_set_of sccs
by forall sccs: set (set vertex). one_in_set_of sccs -> forall cc. not mem cc sccs ->

lemma elt_set_of:
forall x: 'a, cc sccs. mem x cc -> mem cc sccs -> mem x (set_of sccs)

lemma subset_set_of:
forall s s': set (set vertex). subset s s' -> subset (set_of s) (set_of s')

```

#### Ranks and Lists

```lemma elts_cons:
forall x: 'a, l: list 'a. elements (Cons x l) == add x (elements l)

lemma elts_app:
forall s s': list 'a. elements (s ++ s') == union (elements s) (elements s')

lemma list_simpl_r:
forall l1 "induction" l2 l: list 'a. l1 ++ l = l2 ++ l -> l1 = l2

lemma snoc_app:
forall l1 l2: list 'a, x: 'a. (l1 ++ (Cons x Nil)) ++ l2 = l1 ++ (Cons x l2)

predicate is_last (x: 'a) (s: list 'a) =
exists s'. s = s' ++ Cons x Nil

predicate precedes (x y: 'a) (s: list 'a) =
exists s1 s2. s = s1 ++ (Cons x s2) /\ lmem y (Cons x s2)

lemma precedes_mem:
forall x y, s: list 'a. precedes x y s -> lmem x s /\ lmem y s

forall x y, s: list 'a. lmem y (Cons x s) -> precedes x y (Cons x s)

lemma precedes_tail:
forall x y z, s: list 'a. x <> z -> (precedes x y (Cons z s) <-> precedes x y s)

lemma tail_not_precedes:
forall x y, s: list 'a. precedes y x (Cons x s) -> not lmem x s -> y = x

lemma split_list_precedes:
forall x y, s1 s2: list 'a. lmem y (s1 ++ Cons x Nil) -> precedes y x (s1 ++ Cons x s2)

lemma precedes_refl:
forall x, s: list 'a. precedes x x s <-> lmem x s

lemma precedes_append_left:
forall x y, s1 s2: list 'a. precedes x y s1 -> precedes x y (s2 ++ s1)

lemma precedes_append_left_iff:
forall x y, s1 s2: list 'a. not lmem x s1 -> precedes x y (s1 ++ s2) <-> precedes x y s2

lemma precedes_append_right:
forall x y, s1 s2: list 'a. precedes x y s1 -> precedes x y (s1 ++ s2)

lemma precedes_append_right_iff:
forall x y, s1 s2: list 'a. not lmem y s2 -> precedes x y (s1 ++ s2) <-> precedes x y s1

(* simple lists *)

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

lemma simplelist_tl:
forall x: 'a, l. simplelist (Cons x l) -> simplelist l /\ not lmem x l

lemma simplelist_split:
forall x: 'a, l1 "induction" l2 l3 l4. simplelist (l1 ++ Cons x l2)
-> l1 ++ Cons x l2 = l3 ++ Cons x l4 -> l1 = l3 /\ l2 = l4

lemma simplelist_app_disjoint:
forall l1 l2: list 'a. simplelist (l1 ++ l2) -> inter (elements l1) (elements l2) = empty

lemma simplelist_length:
forall s: list 'a. simplelist s -> length s = cardinal (elements s)

lemma precedes_antisym:
forall x y, s: list 'a. simplelist s
-> precedes x y s -> precedes y x s -> x = y

lemma precedes_trans:
forall x y z, s: list 'a. simplelist s
-> precedes x y s -> precedes y z s -> precedes x z s

```

#### Paths

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

lemma reachable_refl:
forall x. reachable x x

lemma reachable_trans:
forall x y z. reachable x y -> reachable y z -> reachable x z

lemma xpath_xedge:
forall x y l s. mem x s -> not mem y s -> path x l y ->
exists x' y'. mem x' s /\ not mem y' s /\ edge x' y' /\ reachable x x' /\ reachable y' y

```

#### Strongly connected components

```
predicate in_same_scc (x y: vertex)  =
reachable x y /\ reachable y x

predicate is_subscc (s: set vertex) =
forall x y. mem x s -> mem y s -> in_same_scc x y

predicate is_scc (s: set vertex) = not is_empty s /\
is_subscc s /\ (forall s'. subset s s' -> is_subscc s' -> s == s')

lemma same_scc_refl:
forall x. in_same_scc x x

lemma same_scc_sym:
forall x z. in_same_scc x z -> in_same_scc z x

lemma same_scc_trans:
forall x y z.
in_same_scc x y -> in_same_scc y z -> in_same_scc x z

forall x y cc. is_subscc cc -> mem x cc -> in_same_scc x y -> is_subscc (add y cc)

lemma scc_max:
forall x y cc. is_scc cc -> mem x cc -> in_same_scc x y -> mem y cc

```

#### Invariant definitions

```constant k_vertex: vertex

axiom k_vertex_not_in_vertices:
not mem k_vertex vertices

type env = {art: set vertex; sn: int; num: map vertex int;
ghost black: set vertex; ghost gray: set vertex}

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

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

predicate is_articulation (x: vertex) =
exists y z. edge y x /\ edge x z
/\ forall l. path y l z -> lmem x l

predicate wf_color (e: env) =
let {black = b; gray = g; art = arts} = e in
subset (union g b) vertices /\
inter b g == empty /\
subset arts b

predicate wf_num (e: env) =
let {black = b; gray = g; sn = n; num = f} = e in
(forall x. -1 <= f[x] < n <= infty() \/ f[x] = infty())  /\
n = cardinal (union g b) /\
(forall x. f[x] = -1 <-> not mem x (union g b))

predicate no_black_to_white (black gray: set vertex) =
forall x x'. edge x x' -> mem x black -> mem x' (union black gray)

predicate wf_env (e: env) = let {black = b; gray = g} = e in
wf_color e /\ wf_num e /\
no_black_to_white b g /\
(forall x. mem x e.art <-> mem x b /\ is_articulation x)

predicate subenv (e e': env) =
subset e.black e'.black /\ subset e.art e'.art /\
e.gray == e'.gray

```

```(*

*)
```

#### auxiliary functions

```
let n = e.sn in
{black = e.black; gray = add x e.gray;
art = e.art; sn = n+1; num = e.num[x <- n]}

let add_black x e =  {black = add x e.black; gray = remove x e.gray;
art = e.art; sn = e.sn; num = e.num}

let add_art x e = {black = e.black; gray = e.gray;
art = add x e.art; sn = e.sn; num = e.num}

```

#### dfs1

```
let test_add_art v x i n e =
if v = k_vertex && i > 1 || v <> k_vertex && n >= e.num[v]
else e

let rec dfs1 v x i e =
requires {mem x vertices}
let (n1, e1) = dfs (successors x) x (add_stack_incr x e) 0 in

```

#### dfs

```
with  dfs roots v e i =
requires {subset roots vertices}
if is_empty roots then (infty(), e) else
let x = choose roots in
let roots' = remove x roots in
let (n1, e1) = if e.num[x] <> -1 then (e.num[x], e) else dfs v x i e in
let (n2, e2) = dfs roots' v e1 (i+1) in (min n1 n2, e2)

```

#### articulation points

```
let articulations () =
let e = {art = empty; sn = 0; num = const (-1);
black = empty; gray = empty } in
let (_, e') = dfs vertices k_vertex e 0 in
e'.art

end

```

#### [session]   [zip, coq2, coq3]

Generated by why3doc 0.88.3