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 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_add_r: forall x: 'a, s1 s2: set 'a. not mem x s2 -> diff s1 (add x s2) == remove x (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
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 -> s = s2 ++ s3 -> 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) = 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.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) = variant {length s} 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 = variant {cardinal (diff vertices (union e.black e.gray)), 0} 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 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 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)}; 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})
with dfs roots e = variant {cardinal (diff vertices (union e.black e.gray)), 1, cardinal roots} 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
Generated by why3doc 0.88.3