(** {1 Depth First Search (nbtw assumption)} The graph is represented by a pair ([vertices], [successor]) {h The algorithm is standard with gray/black sets of nodes. (white set is the union of their complements)
The proof assumes to start with non black-to-white colouring.
All proofs automatic, except Coq used to prove inductive post-condition of dfs_main via lemma no_black_to_white_nopath } *) module Dfs_nbtw 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 use import init_graph.GraphSetSuccPath predicate white_vertex (x: vertex) (v: set vertex) = not (mem x v) predicate white_monotony (v1 v2: set vertex) = forall x: vertex. white_vertex x v2 -> white_vertex x v1 predicate nodeflip (x: vertex) (v1 v2: set vertex) = white_vertex x v1 /\ not (white_vertex x v2) 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 lemma whitepath_mem_decomp: forall x l1 l2 z y v. whitepath x (l1 ++ (Cons y l2)) z v -> whitepath x l1 y v /\ whitepath y (Cons y l2) z v lemma whitepath_mem_decomp_right: forall x l z y v. whitepath x l z v -> L.mem y (l ++ (Cons z Nil)) -> exists l': list vertex. whitepath y l' z v predicate nodeflip_whitepath (roots v1 v2: set vertex) = forall z. nodeflip z v1 v2 -> exists x l. mem x roots /\ whitepath x l z v1 predicate whitepath_nodeflip (roots v1 v2: set vertex) = forall x l z. mem x roots -> whitepath x l z v1 -> nodeflip z v1 v2 predicate reachable (x z: vertex) = exists l. path x l z lemma reachable_succ: forall x x'. edge x x' -> reachable x x' lemma reachable_trans: forall x y z. reachable x y -> reachable y z -> reachable x z predicate access (roots b: set vertex) = forall z. mem z b -> exists x. mem x roots /\ reachable x z lemma access_monotony_l: forall roots roots' b. subset roots roots' -> access roots b -> access roots' b lemma access_monotony_r: forall roots b b'. subset b b' -> access roots b' -> access roots b lemma access_trans: forall roots b b'. access roots b' -> access b' b -> access roots b predicate no_black_to_white (blacks grays: set vertex) = forall x x'. edge x x' -> mem x blacks -> mem x' (union blacks grays) lemma black_to_white_path_goes_thru_gray: forall grays blacks. no_black_to_white blacks grays -> forall x l "induction" z. path x l z -> mem x blacks -> not mem z (union blacks grays) -> exists y. L.mem y l /\ mem y grays (** {3 program} *) let rec dfs (roots grays blacks: set vertex): set vertex variant {(cardinal vertices - cardinal grays), (cardinal roots)} = requires {subset roots vertices} requires {subset grays vertices} requires {no_black_to_white blacks grays} ensures {subset blacks result} ensures {no_black_to_white result grays} ensures {forall x. mem x roots -> not mem x grays -> mem x result} ensures {access (union blacks roots) result} if is_empty roots then blacks else let x = choose roots in let roots' = remove x roots in if mem x (union grays blacks) then dfs roots' grays blacks else let b = dfs (successors x) (add x grays) blacks in assert{ access (add x blacks) b}; dfs roots' grays (union blacks (add x b)) let dfs_main (roots: set vertex) : set vertex = requires {subset roots vertices} ensures {forall s. access roots s <-> subset s result} dfs roots empty empty (** {h Thus the result of dfs_main is exactly the set of nodes reachable from roots } *) end