(** {1 Depth First Search (nbtw assumption)} The graph is represented by a pair ([vertices], [successor]) {h
vertices
: this constant is the set of graph vertices
successor
: this function gives for each vertex the set of vertices directly joinable from it
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