why3doc index index

Abstract Kosaraju 1978 Strongly Connected Components in Graph

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

The algorithm makes two depth-first-search in the graph and its reversed companion. After stacking the vertices in the (post-)order of their visit, one finds the strongly connected components.
Quasi fully automatic proof.

Preamble module

module Kosaraju

  type vertex

  clone export init_graph.GraphSetSucc with type vertex = vertex

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

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

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

  lemma access_from_extension:
    forall x s. access_from x s -> access_from x (add x s)

  predicate access (r s: set vertex) = forall z. mem z s -> exists x. mem x r /\ reachable x z

  lemma access_var:
    forall r r' s. subset r r' -> access r s -> access r' s

  lemma access_covar:
    forall r s s'. subset s s' -> access r s' -> access r s

  lemma access_trans:
    forall r s t. access r s -> access s t -> access r t

  lemma access_from_successors:
    forall x s. mem x vertices -> access (successors x) s -> access_from x s

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

  predicate wf_color (blacks grays: set vertex) = 
    subset blacks vertices /\ subset grays vertices /\
    inter blacks grays = empty /\ 
    nbtw blacks grays

Module SCCK

module SCCK
  use import int.Int
  use import list.List
  use import list.Length
  use import list.Append
  use import list.Reverse 
  use import list.Mem as L
  use import list.NumOcc
  use import list.Elements as E
  use import list.HdTlNoOpt

  type vertex

  clone import Kosaraju as G1 with type vertex = vertex
  clone import Kosaraju as G2 with type vertex = vertex

  axiom reverse_graph:  G1.vertices == G2.vertices /\  (forall x y. G1.edge x y <-> G2.edge y x)

Ranks and Lists

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

  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'

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

(* simple lists *)

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

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


  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_elt:   
    forall s1 s2: set 'a, x: 'a. inter s1 (add x s2) = empty -> not mem x s2 -> inter (add x s1) s2 = empty

  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 elements_add:
    forall x: 'a, l: list 'a. elements (Cons x l) == add x (elements l)

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

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

  lemma elements_elt_exchange:
    forall x y: 'a, l. elements (Cons x (Cons y l)) == elements (Cons y (Cons x l))

  lemma elements_append_comm:
    forall l1 l2: list 'a. elements (l1 ++ l2) == elements (l2 ++ l1)

  lemma subset_inter_subset:
    forall b b' cc: set 'a. subset b b' -> subset cc b' -> subset cc b \/ inter cc (diff b' b) <> empty

Strongly connected components paths

  predicate in_same_scc (x z: vertex)  =
    G1.reachable x z /\ G1.reachable z x

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

  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 cc_ext:
    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

  lemma disjoint_scc:
    forall cc1 cc2. inter cc1 cc2 <> empty -> is_scc cc1 -> is_scc cc2 -> cc1 == cc2

invariants definitions

  predicate reachable_before (x y: vertex) (s: list vertex) = 
   exists l. G1.path x l y /\ (forall z. lmem z (l ++ Cons y Nil) -> lmem z s /\ rank z s <= rank y s) 

  predicate reachable_beforeG2 (x y: vertex) (s: list vertex) = 
   exists l. G2.path x l y /\ (forall z. lmem z (l ++ Cons y Nil) -> lmem z s /\ rank z s <= rank x s)

  predicate reachable_before_same_scc (s: list vertex) =
   forall x y. reachable_before x y s -> in_same_scc x y

  predicate path_in (l: list vertex) (s: list vertex) =
   forall x. lmem x l -> lmem x s
  predicate no_edge_out_of (s s': list vertex) = 
    forall s1. s' = s1 ++ s -> forall x y. lmem x s -> G1.edge x y -> not lmem y s1

  predicate no_path_out_of (s s': list vertex) =
    forall x y l s1. s' = s1 ++ s -> path_in l s' -> lmem x s -> G1.path x l y -> not lmem y s1

  predicate convex_pathsG2 (cc: set vertex) =
    forall x l y. mem x cc -> mem y cc -> G2.path x l y -> forall z. lmem z l -> mem z cc

  predicate wf_stack (blacks grays: set vertex) (s: list vertex) =
    G1.wf_color blacks grays /\ simplelist s /\ elements s == blacks
    /\ subset (elements s) vertices /\ reachable_before_same_scc s

  predicate wf_stackG2 (blacks: set vertex) (s: list vertex) =
    G2.wf_color blacks empty /\ simplelist s /\ subset (elements s) vertices /\
    reachable_before_same_scc s
  lemma wf_stack_white_extension:
    forall b g b' g' s s'. wf_stack b g s -> wf_stack b' g' (s' ++ s) ->
      subset g g' -> forall x. lmem x s' -> not mem x (union b g)

paths reversed, before, out

  lemma reverse_path:
    forall x l y. G1.path x l y -> exists l'. G2.path y l' x /\ reverse (l ++ Cons y Nil) = l' ++ Cons x Nil

  lemma reverse_pathG2:
    forall x l y. G2.path x l y -> exists l'. G1.path y l' x /\ reverse (l ++ Cons y Nil) = l' ++ Cons x Nil

  lemma reachable_before_pop:
    forall x y z s. reachable_before x y (Cons z s) -> lmem y s -> reachable_before x y s

  lemma reachable_before_push:
    forall x y z s. reachable_before x y s -> reachable_before x y (Cons z s)

  lemma reachable_before_reverse:
    forall x y s. reachable_beforeG2 x y s <-> reachable_before y x s

  lemma no_edge_out_push:
    forall s1 s2 x. no_edge_out_of s1 s2 -> (forall z. lmem z s1 -> not G1.edge z x) -> no_edge_out_of s1 (Cons x s2)

  lemma path_cross_sets:
    forall x y s1 s2 l. simplelist (s1 ++ s2) -> lmem y s2 -> lmem x s1 ->
       G1.path y l x -> path_in l (s1 ++ s2) -> exists y' x'. lmem y' s2 /\ lmem x' s1 /\ G1.edge y' x'

  lemma no_edge_out_no_path_out:
    forall s1 s2. simplelist s2 -> no_edge_out_of s1 s2 -> no_path_out_of s1 s2 

  lemma no_black_to_white_no_path_out_of_blacksG2:
    forall b. G2.nbtw b empty -> forall x y l. mem x b -> G2.path x l y -> mem y b

  lemma no_black_to_white_convex_diffG2:
    forall b b'. G2.nbtw b empty -> G2.nbtw b' empty -> subset b b' -> convex_pathsG2 (diff b' b)

  lemma convex_paths_closed_in_sccG2:
    forall x y cc. convex_pathsG2 cc -> in_same_scc x y -> mem x cc -> mem y cc
    by exists l1 l2. G2.path x l1 y /\ G2.path y l2 x


let rec dfs1 r b g s =
requires {subset r G1.vertices} (* R1 *)
(* invariants *)
requires {wf_stack b g s} (* I1a *)
returns{(b', s') -> wf_stack b' g s'} (* I1b *)
(* post conditions *)
returns{(b', _) -> subset r (union b' g)} (* E1 *)
returns {(_, s') -> exists s''. s' = s'' ++ s /\ G1.access r (elements s'')} (* M1 *)  
returns {(b', _) -> subset b b'} (* M2 *)

  if is_empty r then (b, s) else
  let x = choose r in let r' = remove x r in
  let (b1, s1) = 
    if mem x (union b g) then (b, s) else
    let (b2, s2) = dfs1 (G1.successors x) b (add x g) s in
    assert {not lmem x s2};
    assert {(exists s'. Cons x s2 = s' ++ s /\ G1.access_from x (elements s'))
         by exists s''. Cons x s2 = (Cons x s'') ++ s };
    assert {no_path_out_of s (Cons x s2)
         by no_edge_out_of s (Cons x s2)}; 
    (add x b2, Cons x s2) in 
  dfs1 r' b1 g s1


let rec dfs2 r v =
requires {subset r G2.vertices} (* R1 *)
(* invariants *)
requires {G2.wf_color v empty} (* I1a *)
ensures {G2.wf_color result empty} (* I1b *)
(* post conditions *)
ensures {subset r result} (* E1 *)
ensures {G2.access r (diff result v)}
ensures {subset v result} (* M2 *)

  if is_empty r then v else
  let x = choose r in let r' = remove x r in
  let v' = 
    if mem x v then v
    else add x (dfs2 (G2.successors x) v) in
  let v'' = dfs2 r' v' in
  assert {diff v'' v == union (diff v'' v') (diff v' v) };


let rec iter2 s b sccs = 
requires {subset (diff G2.vertices b) (elements s)}
(* invariants *)
requires {wf_stackG2 b s} (* I1a *)
requires {forall cc. mem cc sccs <-> is_scc cc /\ subset cc b} (* I2a *)
returns {(b', _) -> wf_stackG2 b' Nil} (* I1b *)
returns {(b', sccs') -> forall cc. mem cc sccs' <-> is_scc cc /\ subset cc b'} (* I2b *)
(* post conditions *)
returns {(b', _) -> subset (elements s) b'}
returns {(b', _) -> subset b b'}

  match s with
  | Nil -> (b, sccs)
  | Cons x s' ->
    if mem x b then iter2 s' b sccs else
    let b1 = dfs2 (add x empty) b in
    let cc1 = diff b1 b in
    assert {forall y. mem y cc1 -> reachable_before y x s
       by reachable_beforeG2 x y s
       by G2.reachable x y /\ subset cc1 (elements s) /\ convex_pathsG2 cc1 };
    assert {is_subscc cc1 /\ mem x cc1};  
    assert {forall y. in_same_scc y x -> mem y cc1
       by wf_color b empty /\ wf_color b1 empty};
    assert {is_scc cc1};
    iter2 s' b1 (add cc1 sccs)


let scc_main () =
ensures {forall cc. mem cc result <-> is_scc cc /\ subset cc G1.vertices}
  let (_, s) = dfs1 G1.vertices empty empty Nil in
  let (_, sccs) = iter2 s empty empty in 

[session]   [zip]

dfs1 r b g s performs a depth-first search from a set r of roots with given sets b and g of black and gray vertices. It maintains a stack s with the invariant wf_stack b g s. The new set b' and stack s' are the results of dfs1. THe interesting properties of the wf_stack invariants are:

The validity of the wf_stack invariant relies mainly on the non existence of paths between two disjoint subtrees of the spanning tree from left to right. More precisely such a path has to traverse a common ancestor in the spanning tree, i.e. a vertex with a strictly greater serial number in post-order.

dfs2 r v performs a simple depth-first search on the reverse graph G2. It returns the set of vertices accessible from the roots r with an initial set v of already visited vertices.

iter2 s b sccs iterates on the stack s (result of dfs1) with a given set b of black vertices (i.e. already visited) and a set sccs of already computed strongly connected components. In iter2, all vertices are white or black. There are no gray vertices. The stack contains all white vertices, but some of its elements may be black. The set sccs is exactly the set of black strongly connected components. When the top x of the stack is not black, the set cc1 of white vertices accessible from x is computed by dfs2. This set is clearly convex, since no paths between two vertices in cc1 can either go into the already (black) computed SCCs or into the set of white vertices (by saturation of reachability). Therefore a path from any vertex y in cc1 to the top of stack x is fully before x (wrt to post-order). By the invariant wf_stackG2 (which is same as wf_stack on the current stack), the y vertex is in the spanning tree of x (in dfs1) and there is a path from x to y. Hence the set cc1 is a subset of the strongly connected components of x. Moreover it is the SCC by saturation of reachability given by wf_color.

scc_main returns the set of SCCs in graph G1 by calling dfs1 and iter2.

Generated by why3doc 0.88.3