(* 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 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: 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