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 ImpmapNoDom use map.Map use map.Const type key type t 'a = abstract { mutable contents: map key 'a } val function create (x: 'a): t 'a ensures { result.contents = const x } val function ([]) (m: t 'a) (k: key): 'a ensures { result = m.contents[k] } val ghost function ([<-]) (m: t 'a) (k: key) (v: 'a): t 'a ensures { result.contents = m.contents[k <- v] } val ([]<-) (m: t 'a) (k: key) (v: 'a): unit writes { m } ensures { m = (old m)[k <- v] } end module DijkstraShortestPath use int.Int use ref.Ref
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 set.SetImp with type elt = vertex clone ImpmapNoDom with type key = vertex constant v: fset vertex val ghost function g_succ (_x: vertex) : fset vertex ensures { subset result v } val get_succs (x: vertex): set ensures { result = 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: set (* 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: set predicate min (m: vertex) (q: set) (d: t int) = mem m q /\ forall x: vertex. mem x q -> d[m] <= d[x] val q_extract_min () : vertex writes {q} requires { not is_empty q } ensures { min result (old q) d } ensures { q = remove result (old q) } (* Initialisation of visited, q, and d. *) val init (src: vertex) : unit writes { visited, q, d } ensures { is_empty visited } ensures { q = singleton src } ensures { d = (old d)[src <- 0] } (* Relaxation of edge u->v. *) let relax u v ensures { (mem v visited /\ q = old q /\ d = old d) \/ (mem v q /\ d[u] + weight u v >= d[v] /\ q = old q /\ d = old d) \/ (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 mem v visited /\ not mem v (old q) /\ q = add v (old q) /\ d = (old d)[v <- (old d)[u] + weight u v]) } = if not mem v visited then let x = d[u] + weight u v in if mem v q then begin if x < d[v] then d[v] <- x end else begin 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 -> 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) /\ 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' /\ mem v (g_succ v') /\ d' + weight v' v < d lemma Completeness_lemma: forall s: set. (* if s is closed under g_succ *) (forall v: vertex. mem v s -> forall w: vertex. mem w (g_succ v) -> mem w s) -> (* and if s contains src *) forall src: vertex. mem src s -> (* then any vertex reachable from s is also in s *) forall dst: vertex. forall d: int. path src dst d -> mem dst s (* Definitions used in loop invariants. *) predicate inv_src (src: vertex) (s q: set) = mem src s \/ mem src q predicate inv (src: vertex) (s q: set) (d: t int) = inv_src src s q /\ d[src] = 0 /\ (* S and Q are contained in V *) subset s v /\ subset q v /\ (* S and Q are disjoint *) (forall v: vertex. mem v q -> mem v s -> false) /\ (* we already found the shortest paths for vertices in S *) (forall v: vertex. mem v s -> shortest_path src v d[v]) /\ (* there are paths for vertices in Q *) (forall v: vertex. mem v q -> path src v d[v]) predicate inv_succ (_src: vertex) (s q: set) (d: t int) = (* successors of vertices in S are either in S or in Q *) forall x: vertex. mem x s -> forall y: vertex. mem y (g_succ x) -> (mem y s \/ mem y q) /\ d[y] <= d[x] + weight x y predicate inv_succ2 (_src: vertex) (s q: set) (d: t int) (u: vertex) (su: set) = (* successors of vertices in S are either in S or in Q, unless they are successors of u still in su *) forall x: vertex. mem x s -> forall y: vertex. mem y (g_succ x) -> (x<>u \/ (x=u /\ not (mem y su))) -> (mem y s \/ mem y q) /\ d[y] <= d[x] + weight x y lemma inside_or_exit: forall s, src, v, d. mem src s -> path src v d -> mem v s \/ exists y. exists z. exists dy. mem y s /\ not (mem z s) /\ 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 { mem src v /\ mem dst v } ensures { forall v: vertex. mem v visited -> shortest_path src v d[v] } ensures { forall v: vertex. not mem v visited -> forall dv: int. not path src v dv } = init src; while not 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] -> mem x visited } variant { cardinal v - cardinal visited } let u = q_extract_min () in assert { shortest_path src u d[u] }; add u visited; let su = get_succs u in while not is_empty su do invariant { subset su (g_succ u) } invariant { inv src visited q d } invariant { inv_succ2 src visited q d u su } variant { cardinal su } let v = choose_and_remove su in relax u v; assert { d[v] <= d[u] + weight u v } done done end
download ZIP archive