why3doc index index
The graph is represented by a pair (vertices
, successors
)
vertices
: this constant is the set of graph vertices
successors
: this function gives for each vertex the set of vertices directly joinable from it
Notice that this proof uses paths.
module DfsWhitePathSoundness 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 lemma whiteaccess_var: forall r r' s v. subset r r' -> whiteaccess r s v -> whiteaccess r' s v lemma whiteaccess_covar1: forall r s s' v. subset s s' -> whiteaccess r s' v -> whiteaccess r s 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 s v v'. subset v v' -> whiteaccess r s v' -> whiteaccess r s 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 s t v. whiteaccess r s v -> whiteaccess s t v -> whiteaccess r t 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
let rec dfs r v variant {(cardinal vertices - cardinal v), (cardinal r)} = requires {subset r vertices } requires {subset v vertices } ensures {subset v result } ensures {subset result vertices } ensures {whiteaccess r (diff result v) 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 {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 {whiteaccess r' (diff v'' v') v by subset v v' }; assert {diff v'' v == union (diff v'' v') (diff v' v) }; v'' let dfs_main roots = requires {subset roots vertices} ensures {whiteaccess roots result empty so forall z. mem z result -> exists y l. mem y roots /\ path y l z } dfs roots empty end
Generated by why3doc 0.88.3