why3doc index index
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
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 end
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)
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' end 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
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
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)
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) }; 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) end
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 sccs end
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:
nbtw predicate states that there is no edge from a black vertex to a white vertex. It represents the saturation of the black vertices with respect to reachability;
s;
reachable_before_same_scc predicate on the current stack s locates strongly connected components (SCCs) with respect to the rank of vertices in that stack, i.e. wrt to their serial numbers in the post-order traversal of the spanning tree. Thus if a path connects vertices all before (in post-order) the final vertex in this path, the path is inside a same SCC. Therefore each SCC has a maximal vertex (in post-order) whose spanning subtree rooted from it contains a prefix which is this SCC. Notice that this property is expressed by a simple predicate about paths and ranks in the current stack. Notice also that each SCC needs not be a set of contiguous vertices in the current stack.
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