why3doc index index

Abstract Tarjan 1972 Strongly Connected Components in Graph

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

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 SCCTarjan72
  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
  use import array.Array

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

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

Ranks and Lists

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

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

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

function rank (x: 'a) (s: list 'a): int =
  match s with
  | Nil -> max_int()
  | Cons y s' -> if x = y && not (lmem x s') then Length.length s' else rank x s'

lemma rank_not_mem:
  forall x:'a, s. not lmem x s -> rank x s = max_int()

lemma rank_range:
  forall x:'a, s. lmem x s -> 0 <= rank x s < Length.length s

lemma rank_min:
  forall x y:'a, s. is_last x s -> lmem y s -> rank x s <= rank y s

lemma rank_app_l:
  forall x:'a, s s'. lmem x s' -> not lmem x s -> rank x (s' ++ s) = rank x s' + Length.length s

lemma rank_app_r:
  forall x:'a, s s'. lmem x s -> rank x s = rank x (s' ++ s)

(* 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. l1 ++ (Cons x l2) = l3 ++ (Cons x l4) ->
     simplelist (l1 ++ (Cons x l2)) -> l1 = l3 /\ l2 = l4

lemma simplelist_hd_max_rank:
  forall x y: 'a, s1 s2. s1 = Cons x s2 -> simplelist s1 -> lmem y s2 -> rank y s1 < rank x s1

lemma rank_before_suffix:
  forall x y: 'a, s1 s2. simplelist (s1 ++ s2) -> is_last x s1 -> lmem y s2 ->
     rank y (s1 ++ s2) < rank x (s1 ++ s2)


lemma inter_com:
  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 set_elt:
  forall x: 'a, s1 s2 s3: set 'a. not mem x s3 -> union (add x s1) (diff s2 s3) == union s1 (diff (add x s2) s3)

lemma set_mem:
  forall x: 'a, s1 s2 s3 s4: set 'a. s1 == union s2 (diff s3 s4) -> inter s2 s4 == empty -> mem x s1 -> not mem x s4

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

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

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

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

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 simplelist_app_inter:
  forall l1 l2: list 'a. simplelist (l1 ++ l2) -> inter (elements l1) (elements l2) = empty

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

(* sets of sets *)

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

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

axiom set_of_add:
  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 cc sccs /\ mem x cc

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 ->
     one_in_set_of (add 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')


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

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

lemma xset_path_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

lemma subscc_add:
  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

type env = {ghost blacks: set vertex; mutable stack: list int; sccs: set (set int);
          mutable sn: int; num: array int}

predicate wf_color (e: env) (grays: set int) =
  let {stack = s; blacks = b; sccs = ccs} = e in
  subset (union grays b) vertices /\
  inter b grays == empty /\
  elements s == union grays (diff b (set_of ccs)) /\
  subset (set_of ccs) b

predicate wf_num (e: env) (grays: set vertex) =
  let {stack = s; blacks = b; sccs = ccs; sn = n; num = f} = e in
  (forall x. 0 <= x < length f -> -1 <= f[x] < n <= max_int() \/ f[x] = max_int())  /\
  n = cardinal (union grays b) /\
  (forall x. 0 <= x < length f -> f[x] = max_int() <-> mem x (set_of ccs)) /\
  (forall x. 0 <= x < length f -> f[x] = -1 <-> not mem x (union grays b)) /\
  (forall x y. lmem x s -> lmem y s -> f[x] < f[y] <-> rank x s < rank y s)

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

predicate wf_env (e: env) (grays: set vertex) = let s = e.stack in
  wf_color e grays /\ wf_num e grays /\
  no_black_to_white e.blacks grays /\ simplelist s /\
  (forall x y. mem x grays -> lmem y s -> rank x s <= rank y s -> reachable x y) /\
  (forall y. lmem y s -> exists x. mem x grays /\ rank x s <= rank y s /\ reachable y x)

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 num_of_reachable (n: int) (x: vertex) (e: env) =
  exists y. lmem y e.stack /\ n = e.num[y] /\ reachable x y

predicate xedge_to (s1 s3: list vertex) (y: vertex) =
  (exists s2. s1 = s2 ++ s3 /\ exists x. lmem x s2 /\ edge x y) /\ lmem y s3

predicate subenv (e e': env) =
  (exists s. e'.stack = s ++ e.stack /\ subset (elements s) e'.blacks) /\
  subset e.blacks e'.blacks /\ subset e.sccs e'.sccs /\
  (forall x. lmem x e.stack -> e.num[x] = e'.num[x])

4 specialized lemmas

lemma subscc_after_last_gray:
  forall x e g s2 s3. wf_env e (add x g) ->
   let {blacks = b; stack = s} = e in
   s = s2 ++ s3 -> is_last x s2 ->
   subset (elements s2) (add x b) -> is_subscc (elements s2)
      by (access_to (add x g) x
          by inter (add x g) (elements s2) == add x empty)
      /\ access_from x (elements s2)

lemma wf_color_postcond_split:
  forall s2 s3 g b sccs: set vertex. union s2 s3 == union g (diff b sccs) -> inter s2 s3 == empty
        -> inter g s2 == empty -> s3 == union g (diff b (union s2 sccs))

lemma wf_color_sccs:
  forall e g. wf_color e g -> (set_of e.sccs) == diff (union e.blacks g) (elements e.stack)

lemma wf_color_3_cases:
  forall x e g. wf_color e g -> mem x (set_of e.sccs) \/ mem x (elements e.stack) \/ not (mem x (union e.blacks g))

auxiliary functions

let rec split (x : 'a) (s: list 'a) : (list 'a, list 'a) =
returns {(s1, s2) -> s1 ++ s2 = s}
returns {(s1, _) -> lmem x s -> is_last x s1}

  match s with
  | Nil -> (Nil, Nil)
  | Cons y s' -> if x = y then (Cons x Nil, s') else
       let (s1', s2) = split x s' in
        ((Cons y s1'), s2)

let add_stack_incr x e =
requires {0 <= x < cardinal vertices = length e.num}
returns {r -> r.blacks = e.blacks /\ r.sccs = e.sccs /\ r.stack = Cons x e.stack
          /\ r.sn = e.sn + 1 /\ r.num = e.num[x <-e.sn]}
  let n = e.sn in
  e.num[x] <- n;
  {blacks = e.blacks; stack = Cons x e.stack; sccs = e.sccs; sn = n+1; num = e.num}

let add_blacks x e =
returns {r -> r.blacks = add x e.blacks /\ r.stack = e.stack /\ r.sccs = e.sccs
          /\ r.sn = e.sn /\ r.num = e.num}
 {blacks = add x e.blacks; stack = e.stack; sccs = e.sccs; sn = e.sn; num = e.num}

let rec set_max_int (s : list vertex)(f : array int) =
ensures {forall x. lmem x s -> f[x] = max_int()}
ensures {forall x. not lmem x s -> f[x] = (old f)[x] }
  match s with
  | Nil -> ()
  | Cons x s' -> set_max_int s' f; f[x] <- max_int(); ()


let rec dfs1 x e (ghost grays)  =
    let n = e.sn in
    e.stack <- Cons x e.stack; e.sn <- e.sn + 1; e.num[x] <- n;
    let n1 = dfs' (successors x) e (add x grays) in
    let (s2, s3) = split x e.stack in
    if n1 < n then begin
      e.blacks = add x e.blacks;
      n1 end
    else  begin
      set_max_int s2 e.num;
      e.blacks = add x e.blacks; e.stack = s3; e.sccs = add (elements s2) e.sccs;
      max_int() end


with  dfs' roots e (ghost grays) =
  if is_empty roots then max_int()
    let x = choose roots in
    let roots' = remove x roots in
    let n1 = if e.num[x] <> -1 then e.num[x] else dfs1 x e grays in
    let n2 = dfs' roots' e grays in min n1 n2


let tarjan () =
  let n = cardinal vertices in
  let e = {blacks = empty; stack = Nil; sccs = empty; sn = 0; num = make n (-1)} in
  let _  = dfs' vertices e empty in e.sccs


[session coq1 coq2   zip]

Generated by why3doc 0.87.3