# Breadth first search in graph

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
The algorithm is standard bfs in graph. It is derived from generic random ministep search.
The proof is adapted from Dowek and Munoz and is fully automatic.

```
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

```

### program

```
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