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
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 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_not_add_l: forall s1 s2: set 'a, x: 'a. not mem x s2 -> inter (add x s1) s2 == inter s1 s2 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 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') 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') (* 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')
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 -> infty() | 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 = infty() 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. 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) (* simple lists and ranks *) 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)
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
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 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 <= 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] <-> 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
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))
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_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.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 = infty() \/ 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}; (infty(), {blacks = add x e1.blacks; grays = e.grays; stack = s3; sccs = add (elements s2) e1.sccs; sn = e1.sn; num = set_infty s2 e1.num}) end
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 = infty() \/ 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 (infty(), 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)
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
Generated by why3doc 0.88.3