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. Strangely, 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 DFSWhitePathGrayCompteness 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 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' b v. subset r r' -> whiteaccess r b v -> whiteaccess r' b v lemma whiteaccess_minus: 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