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 Bfs use import int.Int use import ref.Ref use import list.List use import list.Length use import list.Mem as L use import list.Elements as E use import list.Append use import queue.Queue use import init_graph.GraphSetSucc use import init_graph.GraphSetSuccPath predicate white_vertex (x: vertex) (v: set vertex) = not (mem x v) 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 predicate whiteaccess (r: set vertex) (z: vertex) (v: set vertex) = exists x l. mem x r /\ whitepath x l z v predicate path_fst_not_twice (x: vertex) (l: list vertex) (z: vertex) = path x l z /\ match l with | Nil -> true | Cons _ l' -> x <> z /\ not (L.mem x l') end lemma path_suffix_fst_not_twice: forall x z l "induction". path x l z -> exists l1 l2. l = l1 ++ l2 /\ path_fst_not_twice x l2 z lemma path_path_fst_not_twice: forall x z l. path x l z -> exists l'. path_fst_not_twice x l' z /\ subset (E.elements l') (E.elements l) predicate whitepath_fst_not_twice (x: vertex) (l: list vertex) (z: vertex) (v: set vertex) = whitepath x l z v /\ path_fst_not_twice x l z lemma whitepath_decomposition: 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_decomposition_r: 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 lemma whitepath_whitepath_fst_not_twice: forall x z l v. whitepath x l z v -> exists l'. whitepath_fst_not_twice x l' z v lemma path_cons_inversion: forall x z l. path x (Cons x l) z -> exists y. edge x y /\ path y l z lemma whitepath_cons_inversion: forall x z l v. whitepath x (Cons x l) z v -> exists y. edge x y /\ whitepath y l z v lemma whitepath_cons_fst_not_twice_inversion: forall x z l v. whitepath_fst_not_twice x (Cons x l) z v -> x <> z -> (exists y. edge x y /\ whitepath y l z (add x v)) lemma whitepath_fst_not_twice_inversion : forall x z l v. whitepath_fst_not_twice x l z v -> x <> z -> (exists y l'. edge x y /\ whitepath y l' z (add x v)) predicate nodeflip_whitepath (roots v1 v2: set vertex) = forall z. nodeflip z v1 v2 -> whiteaccess roots 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
let rec push_set (q: Queue.t vertex) (s: set vertex) variant { cardinal s } = ensures {union (elements (old q.elts)) s == elements q.elts } if not is_empty s then begin let x = choose s in Queue.push x q; push_set q (remove x s) end let rec bfs (roots: Queue.t vertex) (visited: set vertex): set vertex variant {(cardinal vertices - cardinal visited), L.length (roots.elts)} = requires {subset (elements (roots.elts)) vertices } requires {subset visited vertices } raises {Empty} ensures {subset visited result} ensures {whitepath_nodeflip (elements (old roots.elts)) visited result} ensures {nodeflip_whitepath (elements (old roots.elts)) visited result} 'L0: if Queue.is_empty roots then visited else let x = Queue.pop roots in 'L1: if mem x visited then bfs roots visited else begin push_set roots (successors x); 'L2: let r = bfs roots (add x visited) in (*----------- nodeflip_whitepath -----------*) assert {forall z. nodeflip z visited r -> z = x \/ nodeflip z (add x visited) r }; (* case 1-1: nodeflip z visited r /\ z = x *) assert {whitepath x Nil x visited}; (* case 1-2: nodeflip z visited r /\ z <> x *) assert {let roots' = elements (at roots.elts 'L1) in forall z. nodeflip z (add x visited) r -> whiteaccess roots' z (add x visited) \/ whiteaccess (successors x) z (add x visited)}; assert {forall x' l z. whitepath x' l z (add x visited) -> whitepath x' l z visited}; assert {forall z x' l. edge x x' -> whitepath x' l z visited -> whitepath x (Cons x l) z visited}; assert {subset (elements (at roots.elts 'L1))(elements (at roots.elts 'L0))}; assert {subset (elements (at roots.elts 'L2))(union (elements (at roots.elts 'L1)) (successors x))}; assert {forall z. nodeflip z (add x visited) r -> whiteaccess (elements (at roots.elts 'L0)) z visited}; (*-------------- whitepath_nodeflip -------------*) (* case 1: whitepath x l z visited /\ x = z *) assert {mem x r}; (* case 2: whitepath x l z /\ x <> z *) (* using lemma whitepath_whitepath_fst_not_twice *) assert {forall l z. whitepath x l z visited -> x <> z -> exists x' l'. edge x x' /\ whitepath x' l' z (add x visited)}; (* same as lemma whitepath_inversion *) assert {forall l z. whitepath x l z visited -> x <> z -> nodeflip z (add x visited) r}; assert {forall l z. whitepath x l z visited -> nodeflip z visited r}; (* case 3: whitepath roots' l z *) (* case 3-1: whitepath roots' l z /\ L.mem x l *) assert {forall y l z. whitepath y l z visited -> (L.mem x l \/ x = z) -> exists l'. whitepath x l' z visited}; (* goto cases 1-2 *) (* case 3-2: whitepath roots' l z /\ not (L.mem x l) *) assert {let roots' = elements (at roots.elts 'L1) in forall y l z. mem y roots' -> whitepath y l z visited -> not (L.mem x l \/ x = z) -> whitepath y l z (add x visited)}; r end let bfs_main (roots: Queue.t vertex) = requires {subset (elements (roots.elts)) vertices} raises {Empty} bfs roots empty end
Generated by why3doc 0.86.1