## Find the shortest path in a directed graph using BFS

Problem 5 of the second verified software competition.

The ZIP file below contains both the source code, the Why3 proof session file and the Coq scripts of the proofs made in Coq. The Why3 source code is then displayed, followed by a summary of the proofs.

**Authors:** Jean-Christophe Filliâtre

**Topics:** Graph Algorithms

**Tools:** Why3

**References:** The 2nd Verified Software Competition

see also the index (by topic, by tool, by reference, by year)

download ZIP archive

(* The 2nd Verified Software Competition (VSTTE 2012) https://sites.google.com/site/vstte2012/compet Problem 5: Shortest path in a graph using breadth-first search *) theory Graph use import int.Int use export set.Fset type vertex function succ vertex : set vertex (* there is a path of length n from v1 to v2 *) inductive path (v1 v2: vertex) (n: int) = | path_empty: forall v: vertex. path v v 0 | path_succ: forall v1 v2 v3: vertex, n: int. path v1 v2 n -> mem v3 (succ v2) -> path v1 v3 (n+1) (* path length is non-negative *) lemma path_nonneg: forall v1 v2: vertex, n: int. path v1 v2 n -> n >= 0 (* a non-empty path has a last but one node *) lemma path_inversion: forall v1 v3: vertex, n: int. n >= 0 -> path v1 v3 (n+1) -> exists v2: vertex. path v1 v2 n /\ mem v3 (succ v2) (* a path starting in a set S that is closed under succ ends up in S *) lemma path_closure: forall s: set vertex. (forall x: vertex. mem x s -> forall y: vertex. mem y (succ x) -> mem y s) -> forall v1 v2: vertex, n: int. path v1 v2 n -> mem v1 s -> mem v2 s predicate shortest_path (v1 v2: vertex) (n: int) = path v1 v2 n /\ forall m: int. m < n -> not (path v1 v2 m) end module BFS use import int.Int use import Graph use impset.Impset as B use import ref.Refint exception Found int (* global invariant *) predicate inv (s t: vertex) (visited current next: set vertex) (d: int) = (* current *) subset current visited /\ (forall x: vertex. mem x current -> shortest_path s x d) /\ (* next *) subset next visited /\ (forall x: vertex. mem x next -> shortest_path s x (d + 1)) /\ (* visited *) (forall x: vertex, m: int. path s x m -> m <= d -> mem x visited) /\ (forall x: vertex. mem x visited -> exists m: int. path s x m /\ m <= d+1) /\ (* nodes at distance d+1 are either in next or not yet visited *) (forall x: vertex. shortest_path s x (d + 1) -> mem x next \/ not (mem x visited)) /\ (* target t *) (mem t visited -> mem t current \/ mem t next) (* visited\current\next is closed under succ *) predicate closure (visited current next: set vertex) (x: vertex) = mem x visited -> not (mem x current) -> not (mem x next) -> forall y: vertex. mem y (succ x) -> mem y visited (* function fill_next fills set next with the unvisited successors of v *) let fill_next (s t v: vertex) (visited current next: B.t vertex) (d:ref int) requires { inv s t !visited !current !next !d /\ shortest_path s v !d /\ (forall x: vertex. x<> v -> closure !visited !current !next x) } ensures { inv s t !visited !current !next !d /\ subset (succ v) !visited /\ (forall x: vertex. closure !visited !current !next x) } = let acc = ref (succ v) in while not (B.is_empty acc) do invariant { inv s t !visited !current !next !d /\ subset !acc (succ v) /\ subset (diff (succ v) !acc) !visited /\ (forall x: vertex. x<> v -> closure !visited !current !next x) } variant { cardinal !acc } let w = B.pop acc in if not (mem w !visited) then begin B.push w visited; B.push w next end done let bfs (s: vertex) (t: vertex) ensures { forall d: int. not (path s t d) } raises { Found r -> shortest_path s t r } diverges (* the set of reachable nodes may be infinite *) = let visited = ref (singleton s) in let current = ref (singleton s) in let next = ref empty in let d = ref 0 in while not (B.is_empty current) do invariant { inv s t !visited !current !next !d /\ (is_empty !current -> is_empty !next) /\ (forall x: vertex. closure !visited !current !next x) /\ 0 <= !d } let v = B.pop current in if v = t then raise (Found !d); fill_next s t v visited current next d; if B.is_empty current then begin current := !next; next := empty; incr d end done; assert { not (mem t !visited) } end

# Why3 Proof Results for Project "vstte12_bfs"

## Theory "vstte12_bfs.Graph": fully verified in 0.09 s

Obligations | Alt-Ergo (0.95.2) | CVC4 (1.4) | |

path_nonneg | --- | --- | |

induction_pr | |||

1. | 0.02 | 0.00 | |

2. | --- | 0.00 | |

path_inversion | --- | --- | |

inversion_pr | |||

1. | 0.02 | --- | |

2. | 0.00 | --- | |

path_closure | --- | --- | |

induction_pr | |||

1. | 0.02 | 0.02 | |

2. | --- | 0.01 |

## Theory "vstte12_bfs.BFS": fully verified in 11.04 s

Obligations | Alt-Ergo (0.95.2) | Alt-Ergo (0.99.1) | CVC3 (2.4.1) | CVC4 (1.4) | Coq (8.4pl6) | Spass (3.7) | Z3 (3.2) | Z3 (4.3.1) | ||||

VC for fill_next | --- | --- | --- | --- | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||||||

1. loop invariant init | --- | --- | 0.02 | --- | --- | --- | --- | --- | ||||

2. precondition | --- | 0.01 | --- | --- | --- | --- | --- | --- | ||||

3. loop invariant preservation | --- | --- | --- | --- | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||||||

1. VC for fill_next | --- | --- | 3.80 | --- | --- | --- | --- | --- | ||||

2. VC for fill_next | --- | 0.02 | --- | --- | --- | --- | --- | --- | ||||

3. VC for fill_next | --- | 0.04 | --- | --- | --- | --- | --- | --- | ||||

4. VC for fill_next | --- | --- | --- | --- | --- | --- | 0.02 | 0.01 | ||||

4. loop variant decrease | 0.01 | --- | --- | --- | --- | --- | --- | --- | ||||

5. loop invariant preservation | --- | --- | --- | --- | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||||||

1. VC for fill_next | --- | 0.01 | --- | --- | --- | --- | --- | --- | ||||

2. VC for fill_next | --- | 0.01 | --- | --- | --- | --- | --- | --- | ||||

3. VC for fill_next | --- | 0.03 | --- | --- | --- | --- | --- | --- | ||||

4. VC for fill_next | --- | --- | --- | --- | --- | --- | --- | --- | ||||

inline_goal | ||||||||||||

1. VC for fill_next | --- | 0.06 | --- | --- | --- | --- | --- | --- | ||||

6. loop variant decrease | 0.02 | --- | --- | --- | --- | --- | --- | --- | ||||

7. postcondition | --- | --- | --- | --- | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||||||

1. VC for fill_next | --- | 0.01 | --- | --- | --- | --- | --- | --- | ||||

2. VC for fill_next | --- | 0.07 | --- | --- | --- | --- | --- | --- | ||||

3. VC for fill_next | --- | 0.06 | --- | --- | --- | --- | --- | --- | ||||

VC for bfs | --- | --- | --- | --- | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||||||

1. loop invariant init | --- | --- | --- | --- | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||||||

1. VC for bfs | --- | --- | 0.18 | --- | --- | --- | --- | --- | ||||

2. VC for bfs | --- | 0.02 | --- | --- | --- | --- | --- | --- | ||||

3. VC for bfs | --- | --- | --- | --- | --- | --- | --- | --- | ||||

inline_goal | ||||||||||||

1. VC for bfs | --- | 0.01 | --- | --- | --- | --- | --- | --- | ||||

4. VC for bfs | --- | 0.02 | --- | --- | --- | --- | --- | --- | ||||

2. precondition | --- | 0.02 | --- | --- | --- | --- | --- | --- | ||||

3. exceptional postcondition | --- | 0.01 | --- | --- | --- | --- | --- | --- | ||||

4. precondition | --- | --- | --- | --- | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||||||

1. VC for bfs | --- | 0.05 | --- | --- | --- | --- | --- | --- | ||||

2. VC for bfs | --- | 0.01 | --- | --- | --- | --- | --- | --- | ||||

3. VC for bfs | --- | --- | --- | --- | --- | --- | --- | --- | ||||

inline_goal | ||||||||||||

1. VC for bfs | --- | 0.02 | --- | --- | --- | --- | --- | --- | ||||

5. loop invariant preservation | --- | --- | --- | --- | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||||||

1. VC for bfs | --- | --- | --- | --- | --- | --- | --- | --- | ||||

inline_goal | ||||||||||||

1. VC for bfs | --- | --- | --- | --- | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||||||

1. VC for bfs | --- | 0.02 | --- | --- | --- | --- | --- | --- | ||||

2. VC for bfs | --- | 0.02 | --- | --- | --- | --- | --- | --- | ||||

3. VC for bfs | --- | --- | 0.06 | --- | --- | --- | --- | --- | ||||

4. VC for bfs | --- | --- | 0.04 | --- | --- | --- | --- | --- | ||||

5. VC for bfs | --- | --- | --- | 2.24 | --- | --- | --- | --- | ||||

6. VC for bfs | --- | 0.17 | --- | --- | --- | --- | --- | --- | ||||

7. VC for bfs | --- | 0.05 | --- | --- | --- | --- | --- | --- | ||||

8. VC for bfs | --- | 0.08 | --- | --- | --- | --- | --- | --- | ||||

2. VC for bfs | --- | 0.02 | --- | --- | --- | --- | --- | --- | ||||

3. VC for bfs | --- | --- | --- | --- | --- | 2.77 | --- | --- | ||||

4. VC for bfs | --- | 0.01 | --- | --- | --- | --- | --- | --- | ||||

6. loop invariant preservation | --- | --- | --- | --- | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||||||

1. VC for bfs | --- | 0.00 | --- | --- | --- | --- | --- | --- | ||||

2. VC for bfs | --- | 0.01 | --- | --- | --- | --- | --- | --- | ||||

3. VC for bfs | --- | 0.02 | --- | --- | --- | --- | --- | --- | ||||

4. VC for bfs | --- | 0.01 | --- | --- | --- | --- | --- | --- | ||||

7. assertion | --- | 0.02 | --- | 0.01 | --- | --- | --- | --- | ||||

8. postcondition | --- | --- | --- | --- | 0.95 | --- | --- | --- |