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.
module DfsWhitePathCopmleteness 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 ref.Ref use import init_graph.GraphListSucc 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 (roots b v: set vertex) = forall z. mem z b -> exists x l. mem x roots /\ wpath x l z v lemma whiteaccess_union: forall r b1 b2 v. whiteaccess r (union b1 b2) v <-> whiteaccess r b1 v /\ whiteaccess r b2 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 : ref (set vertex)) = requires {subset (elements r) vertices } requires {subset !v vertices } ensures {subset !v vertices } ensures {subset !(old v) !v } ensures {subset (elements r) !v} ensures {nbtw (diff !v !(old v)) !v && forall s. whiteaccess (elements r) s !(old v) -> subset s (diff !v !(old v)) } 'L0: let ghost v0 = !v in match r with | Nil -> () | Cons x r' -> if mem x !v then dfs r' v else begin v := add x !v; dfs (successors x) v; 'L1: let ghost v' = !v in assert {diff v' v0 == add x (diff v' (add x v0)) }; dfs r' v; 'L2: let ghost v'' = !v in assert {diff v'' v0 == union (diff v'' v') (diff v' v0) }; end end end
Generated by why3doc 0.88.3