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 relies on the non-black-to-white property for its completeness.
The set of visited vertices is splitted into gray and black sets.
The result differs from previous dfs versions since only black visited set is returned.
Thus, this proof is slightly more complex than with a sole set of visited vertices.
The formula "A && B" means "A /\ A -> B" .
The formula "A by B" means "B /\ B -> A"
module DFSWhitePathGrayCompleteness 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 whiteaccess (r s v: set vertex) = forall z. mem z s -> exists x l. mem x r /\ wpath x l z v predicate nbtw (b g: set vertex) = forall x x'. edge x x' -> mem x b -> mem x' (union b g) lemma whiteaccess_var: forall r r' s v. subset r r' -> whiteaccess r s v -> whiteaccess r' s v lemma whiteaccess_diff: forall r s v. whiteaccess r s v -> whiteaccess (diff r v) s v lemma nbtw_path: forall r v. nbtw (diff r v) v -> forall x l z. mem x (diff r v) -> wpath x l z v -> mem z (diff r v) lemma nbtw_whiteaccess: forall r s v. nbtw (diff r v) v -> whiteaccess r s v -> subset s (diff r v) lemma diff_empty: forall b g r: set vertex. inter r g == empty -> diff r (union b g) == diff r b lemma whiteaccess_roots_result: forall r r' s v b g. v = union b g -> subset (diff r g) r' -> whiteaccess r s v -> whiteaccess (diff r' v) s v by whiteaccess r' s v by whiteaccess (diff r g) s v by whiteaccess (diff r v) s v
let rec dfs r g b variant {(cardinal vertices - cardinal g), (cardinal r)} = requires {subset r vertices } requires {subset b vertices } requires {subset g vertices } requires {inter b g == empty} ensures {subset result vertices } ensures {subset b result } ensures {inter result g == empty} ensures {subset (diff r g) result && nbtw (diff result (union b g)) (union b g) && forall s. whiteaccess r s (union b g) -> subset s (diff result b) } if is_empty r then b else let x = choose r in let r' = remove x r in let v = union b g in if mem x v then dfs r' g b else let v' = dfs (successors x) (add x g) b in assert {diff (add x v') b == add x (diff v' b) }; let v'' = dfs r' g (add x v') in assert {diff v'' b == union (diff v'' (add x v')) (diff (add x v') b) }; v'' end
Generated by why3doc 0.88.3