examples/dijkstra.mlw

   1
   2 (* Dijkstra's shortest path algorithm.
   3
   4    This proof follows Cormen et al's "Algorithms".
   5
   6    Author: Jean-Christophe Filliâtre (CNRS) *)
   7
   8 module ImpmapNoDom
   9
  10   use map.Map
  11   use map.Const
  12
  13   type key
  14
  15   type t 'a = abstract { mutable contents: map key 'a }
  16
  17   val function create (x: 'a): t 'a
  18     ensures { result.contents = const x }
  19
  20   val function ([]) (m: t 'a) (k: key): 'a
  21     ensures { result = m.contents[k] }
  22
  23   val ghost function ([<-]) (m: t 'a) (k: key) (v: 'a): t 'a
  24     ensures { result.contents = m.contents[k <- v] }
  25
  26   val ([]<-) (m: t 'a) (k: key) (v: 'a): unit
  27     writes { m }
  28     ensures { m = (old m)[k <- v] }
  29
  30 end
  31
  32 module DijkstraShortestPath
  33
  34   use int.Int
  35   use ref.Ref
  36
  37   (** The graph is introduced as a set v of vertices and a function g_succ
  38      returning the successors of a given vertex.
  39      The weight of an edge is defined independently, using function weight.
  40      The weight is an integer. *)
  41
  42   type vertex
  43
  44   clone set.SetImp with type elt = vertex
  45   clone ImpmapNoDom with type key = vertex
  46
  47   constant v: fset vertex
  48
  49   val ghost function g_succ (_x: vertex) : fset vertex
  50     ensures { subset result v }
  51
  52   val get_succs (x: vertex): set
  53     ensures { result = g_succ x  }
  54
  55   val function weight vertex vertex : int (* edge weight, if there is an edge *)
  56     ensures { result >= 0 }
  57
  58   (** Data structures for the algorithm. *)
  59
  60   (* The set of already visited vertices. *)
  61
  62   val visited: set
  63
  64   (* Map d holds the current distances from the source.
  65      There is no need to introduce infinite distances. *)
  66
  67   val d: t int
  68
  69   (* The priority queue. *)
  70
  71   val q: set
  72
  73   predicate min (m: vertex) (q: set) (d: t int) =
  74     mem m q /\
  75     forall x: vertex. mem x q -> d[m] <= d[x]
  76
  77   val q_extract_min () : vertex writes {q}
  78     requires { not is_empty q }
  79     ensures  { min result (old q) d }
  80     ensures  { q = remove result (old q) }
  81
  82   (* Initialisation of visited, q, and d. *)
  83
  84   val init (src: vertex) : unit writes { visited, q, d }
  85     ensures { is_empty visited }
  86     ensures { q = singleton src }
  87     ensures { d = (old d)[src <- 0] }
  88
  89   (* Relaxation of edge u->v. *)
  90
  91   let relax u v
  92     ensures {
  93       (mem v visited /\ q = old q /\ d = old d)
  94       \/
  95       (mem v q /\ d[u] + weight u v >= d[v] /\ q = old q /\ d = old d)
  96       \/
  97       (mem v q /\ (old d)[u] + weight u v < (old d)[v] /\
  98           q = old q /\ d = (old d)[v <- (old d)[u] + weight u v])
  99       \/
 100       (not mem v visited /\ not mem v (old q) /\
 101           q = add v (old q) /\
 102           d = (old d)[v <- (old d)[u] + weight u v]) }
 103   = if not mem v visited then
 104       let x = d[u] + weight u v in
 105       if mem v q then begin
 106         if x < d[v] then d[v] <- x
 107       end else begin
 108         add v q;
 109         d[v] <- x
 110       end
 111
 112   (* Paths and shortest paths.
 113
 114      path x y d =
 115         there is a path from x to y of length d
 116
 117      shortest_path x y d =
 118         there is a path from x to y of length d, and no shorter path *)
 119
 120   inductive path vertex vertex int =
 121     | Path_nil :
 122         forall x: vertex. path x x 0
 123     | Path_cons:
 124         forall x y z: vertex. forall d: int.
 125         path x y d -> mem z (g_succ y) -> path x z (d + weight y z)
 126
 127   lemma Length_nonneg: forall x y: vertex. forall d: int. path x y d -> d >= 0
 128
 129   predicate shortest_path (x y: vertex) (d: int) =
 130     path x y d /\ forall d': int. path x y d' -> d <= d'
 131
 132   lemma Path_inversion:
 133     forall src v:vertex. forall d:int. path src v d ->
 134     (v = src /\ d = 0) \/
 135     (exists v':vertex. path src v' (d - weight v' v) /\ mem v (g_succ v'))
 136
 137   lemma Path_shortest_path:
 138     forall src v: vertex. forall d: int. path src v d ->
 139     exists d': int. shortest_path src v d' /\ d' <= d
 140
 141   (* Lemmas (requiring induction). *)
 142
 143   lemma Main_lemma:
 144     forall src v: vertex. forall d: int.
 145     path src v d -> not (shortest_path src v d) ->
 146     v = src /\ d > 0
 147     \/
 148     exists v': vertex. exists d': int.
 149       shortest_path src v' d' /\ mem v (g_succ v') /\ d' + weight v' v < d
 150
 151   lemma Completeness_lemma:
 152     forall s: set.
 153     (* if s is closed under g_succ *)
 154     (forall v: vertex.
 155        mem v s -> forall w: vertex. mem w (g_succ v) -> mem w s) ->
 156     (* and if s contains src *)
 157     forall src: vertex. mem src s ->
 158     (* then any vertex reachable from s is also in s *)
 159     forall dst: vertex. forall d: int.
 160     path src dst d -> mem dst s
 161
 162   (* Definitions used in loop invariants. *)
 163
 164   predicate inv_src (src: vertex) (s q: set) =
 165     mem src s \/ mem src q
 166
 167   predicate inv (src: vertex) (s q: set) (d: t int) =
 168     inv_src src s q /\ d[src] = 0 /\
 169     (* S and Q are contained in V *)
 170     subset s v /\ subset q v /\
 171     (* S and Q are disjoint *)
 172     (forall v: vertex. mem v q -> mem v s -> false) /\
 173     (* we already found the shortest paths for vertices in S *)
 174     (forall v: vertex. mem v s -> shortest_path src v d[v]) /\
 175     (* there are paths for vertices in Q *)
 176     (forall v: vertex. mem v q -> path src v d[v])
 177
 178   predicate inv_succ (_src: vertex) (s q: set) (d: t int) =
 179     (* successors of vertices in S are either in S or in Q *)
 180     forall x: vertex. mem x s ->
 181     forall y: vertex. mem y (g_succ x) ->
 182     (mem y s \/ mem y q) /\ d[y] <= d[x] + weight x y
 183
 184   predicate inv_succ2 (_src: vertex) (s q: set) (d: t int) (u: vertex) (su: set) =
 185     (* successors of vertices in S are either in S or in Q,
 186        unless they are successors of u still in su *)
 187     forall x: vertex. mem x s ->
 188     forall y: vertex. mem y (g_succ x) ->
 189     (x<>u \/ (x=u /\ not (mem y su))) ->
 190     (mem y s \/ mem y q) /\ d[y] <= d[x] + weight x y
 191
 192  lemma inside_or_exit:
 193     forall s, src, v, d. mem src s -> path src v d ->
 194       mem v s
 195       \/
 196       exists y. exists z. exists dy.
 197         mem y s /\ not (mem z s) /\ mem z (g_succ y) /\
 198         path src y dy /\ (dy + weight y z <= d)
 199
 200   (* Algorithm's code. *)
 201
 202   let shortest_path_code (src dst: vertex)
 203     requires { mem src v /\ mem dst v }
 204     ensures  { forall v: vertex. mem v visited ->
 205                  shortest_path src v d[v] }
 206     ensures  { forall v: vertex. not mem v visited ->
 207                  forall dv: int. not path src v dv }
 208   = init src;
 209     while not is_empty q do
 210       invariant { inv src visited q d }
 211       invariant { inv_succ src visited q d }
 212       invariant { (* vertices at distance < min(Q) are already in S *)
 213                   forall m: vertex. min m q d ->
 214                   forall x: vertex. forall dx: int. path src x dx ->
 215                   dx < d[m] -> mem x visited }
 216       variant   { cardinal v - cardinal visited }
 217       let u = q_extract_min () in
 218       assert { shortest_path src u d[u] };
 219       add u visited;
 220       let su = get_succs u in
 221       while not is_empty su do
 222         invariant { subset su (g_succ u) }
 223         invariant { inv src visited q d  }
 224         invariant { inv_succ2 src visited q d u su }
 225         variant   { cardinal su }
 226         let v = choose_and_remove su in
 227         relax u v;
 228         assert { d[v] <= d[u] + weight u v }
 229       done
 230     done
 231
 232   end