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 DfsWhitePathSoundness use import int.Int use import list.List use import list.Append use import list.Mem as L use import list.Length use import list.Elements as E use import array.Array use import ref.Ref use import init_graph.GraphListArraySucc 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 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)
type color = WHITE | BLACK let rec dfs r (ghost v) col = requires {subset (elements r) vertices } requires {subset !v vertices } requires {Array.length col = cardinal vertices} requires {forall x. mem x !v <-> mem x vertices /\ col[x] = BLACK} ensures {subset !v vertices } ensures {subset !(old v) !v } ensures {forall x. mem x !v <-> mem x vertices /\ col[x] = BLACK} 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 col[x] = BLACK then dfs r' v col else begin v := add x !v; col[x] <- BLACK; dfs (successors x) v col; 'L1: let ghost v' = !v in assert {diff v' v0 == add x (diff v' (add x v0)) }; dfs r' v col; 'L2: let ghost v'' = !v in assert {diff v'' v0 == union (diff v'' v') (diff v' v0) }; end end
(* let rec dfs' r col = match r with | Nil -> () | Cons x r' -> if col[x] = BLACK then dfs' r' col else begin col[x] <- BLACK; dfs' (successors x) col; dfs' r' col; end end let dfs_main' roots = let col = make (cardinal vertices) WHITE in dfs' roots col; let res = ref Nil in for x = 0 to (cardinal vertices) - 1 do if col[x] = BLACK then res := Cons x !res done; !res *) end
Generated by why3doc 0.88.3