Wiki Agenda Contact English version

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.


Auteurs: Jean-Christophe Filliâtre

Catégories: Graph Algorithms

Outils: Why3

Références: 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 int.Int
  use export set.Fset

  type vertex

  val predicate eq (x y: vertex)
    ensures { result <-> x = y }

  function succ vertex : fset 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: fset 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 int.Int
  use Graph
  clone set.SetImp as B with type elt = vertex, val eq = eq
  use ref.Refint

  exception Found int

  (* global invariant *)
  predicate inv (s t: vertex) (visited current next: fset 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: fset 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 (!!) (s: B.set) : fset vertex = B.to_fset s

  val pick_succ (v: vertex) : B.set
    ensures { !!result = succ v }

  (* function fill_next fills set next with the unvisited successors of v *)
  let fill_next (s t v: vertex) (visited current next: B.set) (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 = pick_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.choose_and_remove acc in
      if not (B.mem w visited) then begin
        B.add w visited;
        B.add 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 = B.empty () in
    let current = ref (B.empty ()) in
    let next    = ref (B.empty ()) in
    B.add s visited;
    B.add s !current;
    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.choose_and_remove !current in
      if eq v t then raise (Found !d);
      fill_next s t v visited !current !next d;
      if B.is_empty !current then begin
        (current.contents, next.contents) <- (!next, B.empty ());
        incr d
      end
    done;
    assert { not (mem t !!visited) }

end

Why3 Proof Results for Project "vstte12_bfs"

Theory "vstte12_bfs.Graph": fully verified

ObligationsAlt-Ergo 2.0.0CVC4 1.5
path_nonneg------
induction_pr
path_nonneg.00.00---
path_nonneg.1---0.00
path_inversion------
inversion_pr
path_inversion.00.00---
path_inversion.10.00---
path_closure------
induction_pr
path_closure.00.00---
path_closure.1---0.01

Theory "vstte12_bfs.BFS": fully verified

ObligationsAlt-Ergo 2.0.0CVC4 1.6Coq 8.11.2Eprover 2.0
VC for eq'refn---0.02------
VC for fill_next------------
split_goal_right
loop invariant init0.02---------
precondition0.01---------
loop variant decrease0.02---------
loop invariant preservation------------
introduce_premises
loop invariant preservation------------
inline_goal
loop invariant preservation------------
split_goal_right
VC for fill_next0.03---------
VC for fill_next0.01---------
VC for fill_next0.03---------
VC for fill_next0.04---------
VC for fill_next0.01---------
VC for fill_next0.37---------
VC for fill_next0.01---------
VC for fill_next0.02---------
VC for fill_next0.11---------
VC for fill_next0.01---------
VC for fill_next---------0.42
loop variant decrease0.01---------
loop invariant preservation0.15---------
postcondition0.09---------
VC for bfs------------
split_goal_right
loop invariant init0.04---------
precondition0.00---------
exceptional postcondition0.01---------
precondition------------
split_goal_right
VC for bfs0.02---------
VC for bfs0.01---------
VC for bfs------------
introduce_premises
VC for bfs------------
inline_goal
VC for bfs---------0.34
loop invariant preservation------------
split_goal_right
VC for bfs------------
introduce_premises
VC for bfs------------
inline_goal
VC for bfs------------
split_goal_right
VC for bfs0.01---------
VC for bfs0.01---------
VC for bfs0.02---------
VC for bfs0.02---------
VC for bfs------------
inline_all
VC for bfs---0.21------
VC for bfs0.02---------
VC for bfs0.00---------
VC for bfs0.02---------
VC for bfs0.00---------
VC for bfs------------
introduce_premises
VC for bfs------------
inline_goal
VC for bfs---------0.10
VC for bfs0.01---------
loop invariant preservation0.01---------
assertion0.02---------
postcondition------0.34---