## 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
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] };
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
```