Abstract Tarjan 1972 Strongly Connected Components 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 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

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

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

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

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

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

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

lemma subset_add_r:
  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 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)

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 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 ->
     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')

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

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

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

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

type env = {ghost black: set vertex; ghost gray: set vertex;
          stack: list vertex; sccs: set (set vertex);
          sn: int; num: map vertex int}

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

predicate wf_num (e: env) =
  let {stack = s; black = b; gray = g; sccs = ccs; 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] = infty() <-> mem x (set_of ccs)) /\
  (forall x. f[x] = -1 <-> not mem x (union g b)) /\
  (forall x y. lmem x s -> lmem y s -> f[x] <= f[y] <-> precedes y x s) 

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 {stack = s; black = b; gray = g} = e in
  wf_color e /\ wf_num e /\
  no_black_to_white b g /\ simplelist s /\
  (forall x y. lmem x s -> lmem y s -> e.num[x] <= e.num [y] -> reachable x y) /\
  (forall y. lmem y s -> exists x. mem x g /\ e.num[x] <= e.num[y] /\ reachable y x) /\
  (forall cc. mem cc e.sccs <-> subset cc b /\ is_scc cc)

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

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 splitted (x: 'alpha) (s s1 s2: list 'alpha) =
  s = s1 ++ s2 /\ is_last x s1

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

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. wf_color e -> set_of e.sccs == diff (union e.black e.gray) (elements e.stack)

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

lemma num_lmem:
  forall e x. wf_env e -> 0 <= e.num[x] < infty() <-> lmem x e.stack

lemma num_rank_strict:
    forall e x y. wf_env e -> lmem x e.stack -> lmem y e.stack -> 
       e.num[x] < e.num[y] <-> precedes y x e.stack /\ x <> y

lemma simplelist_x_prec_strict_y':
   forall s1: list 'alpha, s2 s3 x y'. s1 = s2 ++ s3 -> simplelist s1 -> is_last x s2 -> lmem y' s3 ->
     precedes x y' s1 /\ y' <> x

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) 
  end

let add_stack_incr x e =
returns {r -> r.black = e.black /\ r.gray = add x e.gray
          /\ 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
  {black = e.black; gray = add x e.gray; 
   stack = Cons x e.stack; sccs = e.sccs; sn = n+1; num = e.num[x <-n]}

let add_black x e =
returns {r -> r.black = add x e.black /\ r.gray = remove x e.gray 
          /\ r.stack = e.stack /\ r.sccs = e.sccs
          /\ r.sn = e.sn /\ r.num = e.num}
 {black = add x e.black; gray = remove x e.gray; 
  stack = e.stack; sccs = e.sccs; sn = e.sn; num = e.num}

let rec set_infty (s : list vertex)(f : map vertex int) =
returns {f' -> forall x. lmem x s -> f'[x] = infty()}
returns {f' -> forall x. not lmem x s -> f'[x] = f[x] }
  match s with
  | Nil -> f
  | Cons x s' -> (set_infty s' f)[x <- infty()]
  end

let rec dfs1 x e  =
requires {mem x vertices} 
requires {access_to e.gray x} 
requires {not mem x (union e.black e.gray)} 
requires {wf_env e} (* invariant I *)
returns {(_, e') -> wf_env e' /\ subenv e e'} 
(* post-conditions *)
returns {(_, e') -> mem x e'.black} 
returns {(n, e') -> n <= e'.num[x]} 
returns {(n, e') -> n = infty() \/ num_of_reachable n x e'} 
returns {(n, e') -> forall y. xedge_to e'.stack e.stack y -> n <= e'.num[y]}

  let n0 = e.sn in
  let (n1, e1) = dfs (successors x) (add_stack_incr x e) in
  let (s2, s3) = split x e1.stack in 
  assert {is_last x s2 /\ s3 = e.stack /\ subset (elements s2) (add x e1.black)};
  assert {is_subscc (elements s2)};
  if n1 < n0 then begin
    assert {n1 <> infty()};
    assert {exists y. y <> x /\ mem y e1.gray /\ e1.num[y] < e1.num[x] /\ in_same_scc x y};
    (n1, add_black x e1) end
  else begin
    assert {forall y. in_same_scc y x -> lmem y s2};  
    assert {is_scc (elements s2)};
    assert {inter e.gray (elements s2) == empty}; 
    (infty(), {black = add x e1.black; gray = e.gray;
      stack = s3; sccs = add (elements s2) e1.sccs;
      sn = e1.sn; num = set_infty s2 e1.num}) end

with  dfs roots e =
requires {subset roots vertices} 
requires {forall x. mem x roots -> access_to e.gray x} 
requires {wf_env e} (* invariant I *)
returns {(_, e') -> wf_env e' /\ subenv e e'}
(* post-conditions *)
returns {(_, e') -> subset roots (union e'.black e'.gray)} 
returns {(n, e') -> forall x. mem x roots -> n <= e'.num[x]} 
returns {(n, e') -> n = infty() \/ exists x. mem x roots /\ num_of_reachable n x e'} 
returns {(n, e') -> forall y. xedge_to e'.stack e.stack y -> n <= e'.num[y]}

  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 dfs1 x e in
  let (n2, e2) = dfs roots' e1 in (min n1 n2, e2)

let tarjan () =
returns {r -> forall cc. mem cc r <-> subset cc vertices /\ is_scc cc}
  let e = {black = empty; gray = empty; stack = Nil; sccs = empty; sn = 0; num = const (-1)} in
  let (_, e') = dfs vertices e in
    assert {subset vertices e'.black};
    e'.sccs
end