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 int.Int
  use ref.Ref
  use set.Fset

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

  clone impset.Impset as S with type elt = vertex
  clone impmap.ImpmapNoDom with type key = vertex

  constant v: Fset.set vertex

  val ghost function g_succ (x: vertex) : Fset.set vertex
    ensures { Fset.subset result v }

  val get_succs (x: vertex): S.t
    ensures { result.S.contents = g_succ x  }

  val function weight vertex vertex : int (* edge weight, if there is an edge *)
    ensures { result >= 0 }

Data structures for the algorithm.

  (* The set of already visited vertices. *)

  val visited: S.t

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

  val d: t int

  (* The priority queue. *)

  val q: S.t

  predicate min (m: vertex) (q: S.t) (d: t 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.contents = Fset.remove result (old q.S.contents) }

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

  val init (src: vertex) : unit writes { visited, q, d }
    ensures { S.is_empty visited }
    ensures { q.S.contents = Fset.singleton src }
    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.contents = Fset.add v (old q.S.contents) /\
          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[v] <- x
      end else begin
        S.add v q;
        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 -> Fset.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) /\ Fset.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' /\ Fset.mem v (g_succ v') /\ d' + weight v' v < d

  lemma Completeness_lemma:
    forall s: S.t.
    (* if s is closed under g_succ *)
    (forall v: vertex.
       S.mem v s -> forall w: vertex. Fset.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.t) =
    S.mem src s \/ S.mem src q

  predicate inv (src: vertex) (s q: S.t) (d: t int) =
    inv_src src s q /\ d[src] = 0 /\
    (* S and Q are contained in V *)
    Fset.subset s.S.contents v /\ Fset.subset q.S.contents 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.t) (d: t int) =
    (* successors of vertices in S are either in S or in Q *)
    forall x: vertex. S.mem x s ->
    forall y: vertex. Fset.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.t) (d: t int) (u: vertex) (su: S.t) =
    (* 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. Fset.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

 lemma inside_or_exit:
    forall s, src, v, d. S.mem src s -> path src v d ->
      S.mem v s
      \/
      exists y. exists z. exists dy.
        S.mem y s /\ not (S.mem z s) /\ Fset.mem z (g_succ y) /\
        path src y dy /\ (dy + weight y z <= d)

  (* Algorithm's code. *)

  let shortest_path_code (src dst: vertex)
    requires { Fset.mem src v /\ Fset.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 S.is_empty q 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   { Fset.cardinal v - S.cardinal visited }
      let u = q_extract_min () in
      assert { shortest_path src u d[u] };
      S.add u visited;
      let su = get_succs u in
      while not S.is_empty su do
        invariant { Fset.subset su.S.contents (g_succ u) }
        invariant { inv src visited q d  }
        invariant { inv_succ2 src visited q d u su }
        variant   { S.cardinal su }
        let v = S.choose_and_remove su in
        relax u v;
        assert { d[v] <= d[u] + weight u v }
      done
    done

  end

download ZIP archive