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.

This file is with termination proofs by easy lexicographic ordering on number of white vertices and cardinality of roots.



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 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 s' else rank x s'
  end

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

Sets


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

Paths


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; ghost grays: set vertex;
          stack: list vertex; sccs: set (set vertex);
          sn: int; num: map vertex int}

predicate wf_color (e: env) = 
  let {stack = s; blacks = b; grays = 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; blacks = b; grays = g; sccs = ccs; sn = n; num = f} = e in 
  (forall x. -1 <= f[x] < n <= max_int() \/ f[x] = max_int())  /\
  n = cardinal (union g b) /\
  (forall x. f[x] = max_int() <-> 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] <-> 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) = let {stack = s; blacks = b; grays = g} = e in
  wf_color e /\ wf_num e /\
  no_black_to_white b g /\ simplelist s /\
  (forall x y. mem x g -> lmem y s -> rank x s <= rank y s -> reachable x y) /\
  (forall y. lmem y s -> exists x. mem x g /\ 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]) /\
  e.grays == e'.grays

4 specialized lemmas


lemma subscc_after_last_gray:
  forall x e g s2 s3. e.grays == add x g ->  wf_env e ->
   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. wf_color e -> (set_of e.sccs) == diff (union e.blacks e.grays) (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.blacks e.grays))

auxiliary functions

let rec split (x : 'a) (s: list 'a) : (list 'a, list 'a) =
variant {length s}
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.blacks = e.blacks /\ r.grays = add x e.grays
          /\ 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
  {blacks = e.blacks; grays = add x e.grays; 
   stack = Cons x e.stack; sccs = e.sccs; sn = n+1; num = e.num[x <-n]}

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

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

dfs1

let rec dfs1 x e  =
variant{cardinal (diff vertices (union e.blacks e.grays)), 0}
requires {mem x vertices} (* R1 *)
requires {access_to e.grays x} (* R2 *)
requires {not mem x (union e.blacks e.grays)} (* R3 *)
(* invariants *)
requires {wf_env e} (* I1a *)
requires {forall cc. mem cc e.sccs <-> subset cc e.blacks /\ is_scc cc} (* I2a *)
returns {(_, e') -> wf_env e'} (* I1b *)
returns {(_, e') -> forall cc. mem cc e'.sccs <-> subset cc e'.blacks /\ is_scc cc} (* I2b *)
(* post-cond *)
returns {(n, e') -> n <= e'.num[x]} (* PC1 *)
returns {(n, e') -> n = max_int() \/ num_of_reachable n x e'} (* PC2 *)
returns {(n, e') -> forall y. xedge_to e'.stack e.stack y -> n <= e'.num[y]} (* PC3 *)
returns {(_, e') -> mem x e'.blacks} (* PC4 *)
(* monotony *)
returns {(_, e') -> subenv e e'}

    let n = 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.blacks)};
    assert {is_subscc (elements s2)};
    if n1 < n then begin
      assert {exists y. mem y e.grays /\ lmem y e1.stack /\ e1.num[y] < e1.num[x] /\ reachable x y};
      (n1, add_blacks x e1) end
    else  begin
      assert {forall y. in_same_scc y x -> lmem y s2};  
      assert {is_scc (elements s2)};
      assert {inter e.grays (elements s2) = empty by inter e.grays (elements s2) == empty};
      (max_int(), {blacks = add x e1.blacks; grays = e.grays;
         stack = s3; sccs = add (elements s2) e1.sccs;
         sn = e1.sn; num = set_max_int s2 e1.num}) end

dfs


with dfs roots e =
variant {cardinal (diff vertices (union e.blacks e.grays)), 1, cardinal roots}
requires {subset roots vertices} (* R1 *)
requires {forall x. mem x roots -> access_to e.grays x} (* R2 *)
(* invariants *)
requires {wf_env e} (* I1a *)
requires {forall cc. mem cc e.sccs <-> subset cc e.blacks /\ is_scc cc}  (* I2a *)
returns {(_, e') -> wf_env e'} (* I1b *)
returns {(_, e') -> forall cc. mem cc e'.sccs <-> subset cc e'.blacks /\ is_scc cc} (* I2b *)
(* post-cond *)
returns {(n, e') -> forall x. mem x roots -> n <= e'.num[x]} (* PC1 *)
returns {(n, e') -> n = max_int() \/ exists x. mem x roots /\ num_of_reachable n x e'} (* PC2 *)
returns {(n, e') -> forall y. xedge_to e'.stack e.stack y -> n <= e'.num[y]} (* PC3 *)
returns {(_, e') -> subset roots (union e'.blacks e'.grays)} (* PC4 *)
(* monotony *)
returns {(_, e') -> subenv e e'}

  if is_empty roots then (max_int(), e)
  else
    let x = choose roots in
    let roots' = remove x roots in
    let (n1, e1) =
      assert {e.num[x] <> -1 <-> (lmem x e.stack \/ mem x e.blacks)};
      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)

tarjan


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

[session coq1 coq2   zip]



Generated by why3doc 0.87.3