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
module DfsUndirNoWhiteToBlack 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 axiom undirected_graph: forall x y. edge x y -> edge y x predicate nbtw (b g: set vertex) = forall x x'. edge x x' -> mem x b -> mem x' (union b g) predicate nwtb (b g: set vertex) = forall x x'. edge x x' -> mem x' b -> mem x (union b g)
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) && nwtb (diff result (union b g)) (union b g)} 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