Wiki Agenda Contact Version française

Dijkstra's shortest path algorithm


Authors: Jean-Christophe Filliâtre

Topics: Graph Algorithms

Tools: Why3

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


(* Dijkstra's shortest path algorithm.

   This proof follows Cormen et al's "Algorithms".

   Author: Jean-Christophe FilliĆ¢tre (CNRS) *)

module DijkstraShortestPath

  use import int.Int
  use import ref.Ref
  use set.Fset as S
  use import map.Map as M

The graph is introduced as a set v of vertices and a function g_succ returning the successors of a given vertex. The weight of an edge is defined independently, using function weight. The weight is an integer.

  type vertex

  constant v: S.set vertex

  function g_succ vertex : S.set vertex

  axiom G_succ_sound :
    forall x: vertex. S.subset (g_succ x) v

  function weight vertex vertex : int (* edge weight, if there is an edge *)

  axiom Weight_nonneg: forall x y: vertex. weight x y >= 0

Data structures for the algorithm.

  (* The set of already visited vertices. *)

  val visited: ref (S.set vertex)

  val visited_add (x: vertex) : unit writes {visited}
    ensures { !visited = S.add x (old !visited) }

  (* Map d holds the current distances from the source.
     There is no need to introduce infinite distances. *)

  val d: ref (M.map vertex int)

  (* The priority queue. *)

  val q: ref (S.set vertex)

  val q_is_empty () : bool
    ensures { result = True <-> S.is_empty !q }

  predicate min (m: vertex) (q: S.set vertex) (d: M.map vertex int) =
    S.mem m q /\
    forall x: vertex. S.mem x q -> d[m] <= d[x]

  val q_extract_min () : vertex writes {q}
    requires { not S.is_empty !q }
    ensures  { min result (old !q) !d }
    ensures  { !q = S.remove result (old !q) }

  (* Initialisation of visited, q, and d. *)

  val init (src: vertex) : unit writes { visited, q, d }
    ensures { S.is_empty !visited }
    ensures { !q = S.add src S.empty }
    ensures { !d = (old !d)[src <- 0] }

  (* Relaxation of edge u->v. *)

  let relax u v
    ensures {
      (S.mem v !visited /\ !q = old !q /\ !d = old !d)
      \/
      (S.mem v !q /\ !d[u] + weight u v >= !d[v] /\
          !q = old !q /\ !d = old !d)
      \/
      (S.mem v !q /\ (old !d)[u] + weight u v < (old !d)[v] /\
          !q = old !q /\ !d = (old !d)[v <- (old !d)[u] + weight u v])
      \/
      (not S.mem v !visited /\ not S.mem v (old !q) /\ !q = S.add v (old !q) /\
          !d = (old !d)[v <- (old !d)[u] + weight u v]) }
  = if not (S.mem v !visited) then
      let x = !d[u] + weight u v in
      if S.mem v !q then begin
        if x < !d[v] then d := !d[v <- x]
      end else begin
        q := S.add v !q;
        d := !d[v <- x]
      end

  (* Paths and shortest paths.

     path x y d =
        there is a path from x to y of length d

     shortest_path x y d =
        there is a path from x to y of length d, and no shorter path *)

  inductive path vertex vertex int =
    | Path_nil :
        forall x: vertex. path x x 0
    | Path_cons:
        forall x y z: vertex. forall d: int.
        path x y d -> S.mem z (g_succ y) -> path x z (d + weight y z)

  lemma Length_nonneg: forall x y: vertex. forall d: int. path x y d -> d >= 0

  predicate shortest_path (x y: vertex) (d: int) =
    path x y d /\ forall d': int. path x y d' -> d <= d'

  lemma Path_inversion:
    forall src v:vertex. forall d:int. path src v d ->
    (v = src /\ d = 0) \/
    (exists v':vertex. path src v' (d - weight v' v) /\ S.mem v (g_succ v'))

  lemma Path_shortest_path:
    forall src v: vertex. forall d: int. path src v d ->
    exists d': int. shortest_path src v d' /\ d' <= d

  (* Lemmas (requiring induction). *)

  lemma Main_lemma:
    forall src v: vertex. forall d: int.
    path src v d -> not (shortest_path src v d) ->
    v = src /\ d > 0
    \/
    exists v': vertex. exists d': int.
      shortest_path src v' d' /\ S.mem v (g_succ v') /\ d' + weight v' v < d

  lemma Completeness_lemma:
    forall s: S.set vertex.
    (* if s is closed under g_succ *)
    (forall v: vertex.
       S.mem v s -> forall w: vertex. S.mem w (g_succ v) -> S.mem w s) ->
    (* and if s contains src *)
    forall src: vertex. S.mem src s ->
    (* then any vertex reachable from s is also in s *)
    forall dst: vertex. forall d: int.
    path src dst d -> S.mem dst s

  (* Definitions used in loop invariants. *)

  predicate inv_src (src: vertex) (s q: S.set vertex) =
    S.mem src s \/ S.mem src q

  predicate inv (src: vertex) (s q: S.set vertex) (d: M.map vertex int) =
    inv_src src s q /\ d[src] = 0 /\
    (* S and Q are contained in V *)
    S.subset s v /\ S.subset q v /\
    (* S and Q are disjoint *)
    (forall v: vertex. S.mem v q -> S.mem v s -> false) /\
    (* we already found the shortest paths for vertices in S *)
    (forall v: vertex. S.mem v s -> shortest_path src v d[v]) /\
    (* there are paths for vertices in Q *)
    (forall v: vertex. S.mem v q -> path src v d[v])

  predicate inv_succ (src: vertex) (s q: S.set vertex) (d: M.map vertex int) =
    (* successors of vertices in S are either in S or in Q *)
    forall x: vertex. S.mem x s ->
    forall y: vertex. S.mem y (g_succ x) ->
    (S.mem y s \/ S.mem y q) /\ d[y] <= d[x] + weight x y

  predicate inv_succ2 (src: vertex) (s q: S.set vertex) (d: M.map vertex int)
                      (u: vertex) (su: S.set vertex) =
    (* successors of vertices in S are either in S or in Q,
       unless they are successors of u still in su *)
    forall x: vertex. S.mem x s ->
    forall y: vertex. S.mem y (g_succ x) ->
    (x<>u \/ (x=u /\ not (S.mem y su))) ->
    (S.mem y s \/ S.mem y q) /\ d[y] <= d[x] + weight x y

  (* Iteration on a set *)

  val set_has_next (s: ref (S.set 'a)) : bool
    ensures { result = True <-> not (S.is_empty !s) }

  val set_next (s: ref (S.set 'a)) : 'a writes {s}
    requires { not S.is_empty !s }
    ensures  { S.mem result (old !s) }
    ensures  { !s = S.remove result (old !s) }

  (* Algorithm's code. *)

  let shortest_path_code (src dst: vertex)
    requires { S.mem src v /\ S.mem dst v }
    ensures  { forall v: vertex. S.mem v !visited ->
                 shortest_path src v !d[v] }
    ensures  { forall v: vertex. not S.mem v !visited ->
                 forall dv: int. not path src v dv }
  = init src;
    while not (q_is_empty ()) do
      invariant { inv src !visited !q !d }
      invariant { inv_succ src !visited !q !d }
      invariant { (* vertices at distance < min(Q) are already in S *)
                  forall m: vertex. min m !q !d ->
                  forall x: vertex. forall dx: int. path src x dx ->
                  dx < !d[m] -> S.mem x !visited }
      variant   { S.cardinal v - S.cardinal !visited }
      let u = q_extract_min () in
      assert { shortest_path src u !d[u] };
      visited_add u;
      let su = ref (g_succ u) in
      while set_has_next su do
        invariant { S.subset !su (g_succ u) }
        invariant { inv src !visited !q !d  }
        invariant { inv_succ2 src !visited !q !d u !su }
        variant   { S.cardinal !su }
        let v = set_next su in
        relax u v;
        assert { !d[v] <= !d[u] + weight u v }
      done
    done

  end

download ZIP archive