why3doc index index
The graph is represented by a pair (vertices, successor)
vertices : this constant is the set of graph vertices
successors : this function gives for each vertex the set of vertices directly joinable from it
module ArtTarjan72 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_not_add_l: forall x: 'a, s1 s2: set 'a. mem x s2 -> diff (add x s1) s2 == 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
constant k_vertex: vertex axiom k_vertex_not_in_vertices: not mem k_vertex vertices type env = {art: set vertex; sn: int; num: map vertex int; ghost black: set vertex; ghost gray: set vertex} 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 is_articulation (x: vertex) = exists y z. edge y x /\ edge x z /\ forall l. path y l z -> lmem x l predicate wf_color (e: env) = let {black = b; gray = g; art = arts} = e in subset (union g b) vertices /\ inter b g == empty /\ subset arts b predicate wf_num (e: env) = let {black = b; gray = g; 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] = -1 <-> not mem x (union g b)) 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 {black = b; gray = g} = e in wf_color e /\ wf_num e /\ no_black_to_white b g /\ (forall x. mem x e.art <-> mem x b /\ is_articulation x) predicate subenv (e e': env) = subset e.black e'.black /\ subset e.art e'.art /\ e.gray == e'.gray
(*
*)
let add_stack_incr x e = let n = e.sn in {black = e.black; gray = add x e.gray; art = e.art; sn = n+1; num = e.num[x <- n]} let add_black x e = {black = add x e.black; gray = remove x e.gray; art = e.art; sn = e.sn; num = e.num} let add_art x e = {black = e.black; gray = e.gray; art = add x e.art; sn = e.sn; num = e.num}
let test_add_art v x i n e = if v = k_vertex && i > 1 || v <> k_vertex && n >= e.num[v] then add_art v e else e let rec dfs1 v x i e = requires {mem x vertices} let (n1, e1) = dfs (successors x) x (add_stack_incr x e) 0 in (n1, add_black (n0, test_add_art v x i n0 e0))
with dfs roots v e i = requires {subset roots vertices} 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 dfs v x i e in let (n2, e2) = dfs roots' v e1 (i+1) in (min n1 n2, e2)
let articulations () = let e = {art = empty; sn = 0; num = const (-1); black = empty; gray = empty } in let (_, e') = dfs vertices k_vertex e 0 in e'.art end
Generated by why3doc 0.88.3