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
Notice that this proof uses paths for the soundness part, but relies on the non-black-to-white property for its completeness.
This proof is close to the one in Cormen et al.; but is simpler since
there is no need for the so-called Parenthesis theorem, nor for a
time variable. The present proof follows from the structure of the
recursion.
The formula "A && B" means "A /\ A -> B" .
The formula "A by B" means "B /\ B -> A"
module DfsWhitePathThm use import int.Int use import list.List use import list.Append use import list.Mem as L use import list.Elements as E use import init_graph.GraphSetSucc predicate white_vertex (x: vertex) (v: set vertex) = not (mem x v) inductive wpath vertex (list vertex) vertex (set vertex) = | WPath_empty: forall x v. white_vertex x v -> wpath x Nil x v | WPath_cons: forall x y l z v. white_vertex x v -> edge x y -> wpath y l z v -> wpath x (Cons x l) z v (* predicate whitepath (x: vertex) (l: list vertex) (z: vertex) (v: set vertex) = path x l z /\ (forall y. L.mem y l -> white_vertex y v) /\ white_vertex z v *) predicate whiteaccess (roots b v: set vertex) = forall z. mem z b -> exists x l. mem x roots /\ wpath x l z v lemma whiteaccess_var: forall r r' b v. subset r r' -> whiteaccess r b v -> whiteaccess r' b v lemma whiteaccess_covar1: forall r b b' v. subset b b' -> whiteaccess r b' v -> whiteaccess r b v lemma wpath_covar2: forall x l z v v'. subset v v' -> wpath x l z v' -> wpath x l z v lemma whiteaccess_covar2: forall r b v v'. subset v v' -> whiteaccess r b v' -> whiteaccess r b v lemma wpath_trans: forall x l y l' z v. wpath x l y v -> wpath y l' z v -> wpath x (l ++ l') z v lemma whiteaccess_trans: forall r r' b v. whiteaccess r r' v -> whiteaccess r' b v -> whiteaccess r b v lemma whiteaccess_cons: forall x s v. mem x vertices -> white_vertex x v -> whiteaccess (successors x) s v -> whiteaccess (add x empty) s v predicate nbtw (b v: set vertex) = forall x x'. edge x x' -> mem x b -> mem x' (union b v) lemma nbtw_path: forall v v'. nbtw (diff v' v) v' -> forall x l z. mem x (diff v' v) -> wpath x l z v -> mem z (diff v' v)
let rec dfs r v variant {(cardinal vertices - cardinal v), (cardinal r)} = requires {subset r vertices } requires {subset v vertices } ensures {subset result vertices } ensures {subset v result } ensures {subset r result } ensures {nbtw (diff result v) result && forall s. whiteaccess r s v <-> subset s (diff result v) } if is_empty r then v else let x = choose r in let r' = remove x r in if mem x v then dfs r' v else let v' = dfs (successors x) (add x v) in assert {whiteaccess (add x empty) (diff v' (add x v)) v by whiteaccess (successors x) (diff v' (add x v)) v by subset (diff v' (add x v)) (diff v' v) by subset v (add x v) }; assert {wpath x Nil x v }; assert {whiteaccess (add x empty) (diff v' v) v by diff v' v == add x (diff v' (add x v)) }; let v'' = dfs r' v' in assert {diff v'' v == union (diff v'' v') (diff v' v) }; assert {whiteaccess r' (diff v'' v') v by subset v v' }; v'' end
Generated by why3doc 0.88.3