mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
233 lines
6.8 KiB
Plaintext
233 lines
6.8 KiB
Plaintext
|
|
(* 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
|