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 DagTest 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 list.HdTlNoOpt use import init_graph.GraphSetSucc use import map.Map use import ref.Ref use import ref.Refint predicate lmem (x: 'a) (s: list 'a) = L.mem x s
(* simple lists *) predicate simplelist (l: list 'a) = forall x. num_occ x l <= 1
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_subset_inter: forall s1 s2 s3: set 'a. inter s1 s2 = empty -> subset s3 s2 -> inter s1 s3 = empty lemma subset_add: forall x: 'a, s s': set 'a. subset s' (add x s) -> mem x s' \/ subset s' 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 no_black_to_gray (blacks grays: set vertex) = forall x x'. edge x x' -> mem x blacks -> not mem x' grays predicate circle (x: vertex) (l: list vertex) = l <> Nil /\ simplelist l /\ path x l x predicate black_circle (x: vertex) (l: list vertex) (b: set vertex) = circle x l /\ subset (elements l) b predicate reachable (x z: vertex) = exists l. path x l z predicate access_to (s: set vertex) (y: vertex) = forall x. mem x s -> reachable x y
use import list.Permut lemma circle_rotate: forall x y l1 l2. circle x (Cons x (l1 ++ Cons y l2)) -> circle y (Cons y (l2 ++ Cons x l1)) let lemma circle_rotate_to (x y: vertex) (l: list vertex) requires {circle x l} requires {lmem y l} ensures {exists l'. circle y l' /\ permut l l'} = if y = x then () else assert {exists l1 l2. l = Cons x l1 ++ Cons y l2}; ()
predicate wff_color (blacks grays: set vertex) = no_black_to_white blacks grays /\ no_black_to_gray blacks grays /\ inter blacks grays = empty use import list.Reverse predicate gray_chain_edge (s: list vertex) (x: vertex) = s <> Nil -> edge (hd s) x /\ path (hd (reverse s)) (reverse s) x /\ simplelist s lemma simple_list_decomp: forall l1 l2: list 'a. simplelist (l1 ++ l2) -> simplelist l1 /\ simplelist l2 lemma simple_non_empty_path_decomp_general: forall x l z y. path x l z -> simplelist l -> lmem y l -> exists l'. path y l' z /\ simplelist l' /\ l' <> Nil let rec dfs1 x blacks grays (ghost stack) = requires {mem x vertices} requires {grays == elements stack} requires {gray_chain_edge stack x} requires {not mem x (union blacks grays)} (* invariants *) requires {wff_color blacks grays} requires {forall x l. not black_circle x l blacks} returns {(r, b) -> r -> wff_color b grays} returns {(r, b) -> r -> forall x l. not black_circle x l b} returns {(r, _) -> not r -> exists x l. circle x l} (* post-conditions *) returns {(_, b) -> mem x b} (* monotony *) returns {(_, b) -> subset blacks b} let (r1, b1) = dfs' (successors x) blacks (add x grays) (Cons x stack) in assert {forall y l. black_circle y l (add x b1) -> lmem x l -> exists l'. black_circle x l' (add x b1)}; assert {forall l. black_circle x l (add x b1) -> exists y. edge y x /\ mem y (add x b1)}; (r1, add x b1)
with dfs' roots blacks grays (ghost stack) = requires {subset roots vertices} requires {grays == elements stack} requires {forall x. mem x roots -> gray_chain_edge stack x} (* invariants *) requires {wff_color blacks grays} requires {forall x l. not black_circle x l blacks} returns {(r, b) -> r -> wff_color b grays} returns {(r, b) -> r -> forall x l. not black_circle x l b} returns {(r, _) -> r = false -> exists x l. circle x l} (* post-conditions *) returns {(r, b) -> r -> subset roots b} (* monotony *) returns {(_, b) -> subset blacks b} if is_empty roots then (true, blacks) else let y = choose roots in let roots' = remove y roots in if mem y grays then (false, blacks) else let (r3, b3) = if mem y blacks then (true, blacks) else dfs1 y blacks grays stack in if r3 then dfs' roots' b3 grays stack else (false, b3) let dag_main () = returns {(r, _) -> r = not exists x l. circle x l /\ subset (elements l) vertices} dfs' vertices empty empty Nil
end
Generated by why3doc 0.87.0