examples/bellman_ford.mlw

   1
   2 (** {1 A proof of Bellman-Ford algorithm}
   3
   4    By Yuto Takei (University of Tokyo, Japan)
   5    and Jean-Christophe Filliâtre (CNRS, France). *)
   6
   7 theory Graph
   8
   9   use export list.List
  10   use export list.Append
  11   use export list.Length
  12   use export int.Int
  13   use export set.Fset
  14
  15   (* the graph is defined by a set of vertices and a set of edges *)
  16   type vertex
  17   constant vertices: fset vertex
  18   constant edges: fset (vertex, vertex)
  19
  20   predicate edge (x y: vertex) = mem (x,y) edges
  21
  22   (* edges are well-formed *)
  23   axiom edges_def:
  24     forall x y: vertex.
  25     mem (x, y) edges -> mem x vertices /\ mem y vertices
  26
  27   (* a single source vertex s is given *)
  28   val constant s: vertex
  29     ensures { mem result vertices }
  30
  31   (* hence vertices is non empty *)
  32   lemma vertices_cardinal_pos: cardinal vertices > 0
  33
  34   val constant nb_vertices: int
  35     ensures { result = cardinal vertices }
  36
  37   (* paths *)
  38   clone export graph.IntPathWeight
  39      with type vertex = vertex, predicate edge = edge
  40
  41   lemma path_in_vertices:
  42     forall v1 v2: vertex, l: list vertex.
  43     mem v1 vertices -> path v1 l v2 -> mem v2 vertices
  44
  45   (* A key idea behind Bellman-Ford's correctness is that of simple path:
  46      if there is a path from s to v, there is a path with less than
  47      |V| edges. We formulate this in a slightly more precise way: if there
  48      a path from s to v with at least |V| edges, then there must be a duplicate
  49      vertex along this path. There is a subtlety here: since the last vertex
  50      of a path is not part of the vertex list, we distinguish the case where
  51      the duplicate vertex is the final vertex v.
  52
  53      Proof: Assume [path s l v] with length l >= |V|.
  54        Consider the function f mapping i in {0..|V|} to the i-th element
  55        of the list l ++ [v]. Since all elements of the
  56        path (those in l and v) belong to V, then by the pigeon hole principle,
  57        f cannot be injective from 0..|V| to V. Thus there exist two distinct
  58        i and j in 0..|V| such that f(i)=f(j), which means that
  59               l ++ [v] = l1 ++ [u] ++ l2 ++ [u] ++ l3
  60        Two cases depending on l3=[] (and thus u=v) conclude the proof. Qed.
  61   *)
  62
  63   clone pigeon.ListAndSet with type t = vertex
  64
  65   predicate cyc_decomp (v: vertex) (l: list vertex)
  66                        (vi: vertex) (l1 l2 l3: list vertex) =
  67     l = l1 ++ l2 ++ l3 /\ length l2 > 0 /\
  68     path s l1 vi /\ path vi l2 vi /\ path vi l3 v
  69
  70   lemma long_path_decomposition:
  71     forall l v. path s l v /\ length l >= cardinal vertices ->
  72       (exists vi l1 l2 l3. cyc_decomp v l vi l1 l2 l3)
  73       by exists n l1 l2 l3. Cons v l = l1 ++ Cons n (l2 ++ Cons n l3)
  74       so match l1 with
  75         | Nil -> cyc_decomp v l v l2 (Cons n l3) Nil
  76         | Cons v l1 -> cyc_decomp v l n l1 (Cons n l2) (Cons n l3)
  77         end
  78
  79   lemma long_path_reduction:
  80     forall l v. path s l v /\ length l >= cardinal vertices ->
  81       exists l'. path s l' v /\ length l' < length l
  82       by exists vi l1 l2 l3. cyc_decomp v l vi l1 l2 l3 /\ l' = l1 ++ l3
  83
  84   let lemma simple_path (v: vertex) (l: list vertex) : unit
  85     requires { path s l v }
  86     ensures  { exists l'. path s l' v /\ length l' < cardinal vertices }
  87   = let rec aux (n: int) : unit
  88       ensures { forall l. length l <= n /\ path s l v ->
  89           exists l'. path s l' v /\ length l' < cardinal vertices }
  90       variant { n }
  91     = if n > 0 then aux (n-1)
  92     in
  93     aux (length l)
  94
  95   (* negative cycle [v] -> [v] reachable from [s] *)
  96   predicate negative_cycle (v: vertex) =
  97     mem v vertices /\
  98     (exists l1: list vertex. path s l1 v) /\
  99     (exists l2: list vertex. path v l2 v /\ path_weight l2 v < 0)
 100
 101   (* key lemma for existence of a negative cycle
 102
 103      Proof: by induction on the (list) length of the shorter path l
 104        If length l < cardinal vertices, then it contradicts hypothesis 1
 105        thus length l >= cardinal vertices and thus the path contains a cycle
 106              s ----> n ----> n ----> v
 107        If the weight of the cycle n--->n is negative, we are done.
 108        Otherwise, we can remove this cycle from the path and we get
 109        an even shorter path, with a stricltly shorter (list) length,
 110        thus we can apply the induction hypothesis.                     Qed.
 111    *)
 112   predicate all_path_gt (v: vertex) (n: int) =
 113     forall l. path s l v /\ length l < cardinal vertices -> path_weight l v >= n
 114
 115   let lemma key_lemma_1 (v: vertex) (l: list vertex) (n: int) : unit
 116     (* if any simple path has weight at least n *)
 117     requires { all_path_gt v n }
 118     (* and if there exists a shorter path *)
 119     requires { path s l v /\ path_weight l v < n }
 120     (* then there exists a negative cycle. *)
 121     ensures  { exists u. negative_cycle u }
 122   = let rec aux (m: int) : (_a: 'a)
 123       requires { forall u. not negative_cycle u }
 124       requires { exists l. path s l v /\ path_weight l v < n /\ length l <= m }
 125       ensures  { false }
 126       variant  { m }
 127     = assert { (exists l'. path s l' v /\ path_weight l' v < n /\ length l' < m)
 128         by exists l. path s l v /\ path_weight l v < n /\ length l <= m
 129         so exists vi l1 l2 l3. cyc_decomp v l vi l1 l2 l3
 130         so let res = l1 ++ l3 in
 131           path s res v /\ length res < length l /\ path_weight res v < n
 132           by path_weight l v =
 133             path_weight l1 vi + path_weight l2 vi + path_weight l3 v
 134           so path_weight l2 vi >= 0 by not negative_cycle vi
 135       };
 136       aux (m-1)
 137     in
 138     if pure { forall u. not negative_cycle u } then aux (length l)
 139
 140 end
 141
 142 module ImpmapNoDom
 143
 144   use map.Map
 145   use map.Const
 146
 147   type key
 148
 149   type t 'a = abstract { mutable contents: map key 'a }
 150
 151   val function create (x: 'a): t 'a
 152     ensures { result.contents = const x }
 153
 154   val function ([]) (m: t 'a) (k: key): 'a
 155     ensures { result = m.contents[k] }
 156
 157   val ghost function ([<-]) (m: t 'a) (k: key) (v: 'a): t 'a
 158     ensures { result.contents = m.contents[k <- v] }
 159
 160   val ([]<-) (m: t 'a) (k: key) (v: 'a): unit
 161     writes { m }
 162     ensures { m = (old m)[k <- v] }
 163
 164 end
 165
 166 module BellmanFord
 167
 168   use Graph
 169   use int.IntInf as D
 170   use ref.Ref
 171   clone set.SetImp as S with type elt = (vertex, vertex)
 172   clone ImpmapNoDom with type key = vertex
 173
 174   type distmap = ImpmapNoDom.t D.t
 175
 176   let initialize_single_source (s: vertex): distmap
 177     ensures { result = (create D.Infinite)[s <- D.Finite 0] }
 178   =
 179     let m = create D.Infinite in
 180     m[s] <- D.Finite 0;
 181     m
 182
 183   (* [inv1 m pass via] means that we already performed [pass-1] steps
 184      of the main loop, and, in step [pass], we already processed edges
 185      in [via] *)
 186   predicate inv1 (m: distmap) (pass: int) (via: fset (vertex, vertex)) =
 187     forall v: vertex. mem v vertices ->
 188     match m[v] with
 189       | D.Finite n ->
 190         (* there exists a path of weight [n] *)
 191         (exists l: list vertex. path s l v /\ path_weight l v = n) /\
 192         (* there is no shorter path in less than [pass] steps *)
 193         (forall l: list vertex.
 194            path s l v -> length l < pass -> path_weight l v >= n) /\
 195         (* and no shorter path in i steps with last edge in [via] *)
 196         (forall u: vertex, l: list vertex.
 197            path s l u -> length l < pass -> mem (u,v) via ->
 198            path_weight l u + weight u v >= n)
 199       | D.Infinite ->
 200         (* any path has at least [pass] steps *)
 201         (forall l: list vertex. path s l v -> length l >= pass) /\
 202         (* [v] cannot be reached by [(u,v)] in [via] *)
 203         (forall u: vertex. mem (u,v) via -> (*m[u] = D.Infinite*)
 204           forall lu: list vertex. path s lu u -> length lu >= pass)
 205     end
 206
 207   predicate inv2 (m: distmap) (via: fset (vertex, vertex)) =
 208     forall u v: vertex. mem (u, v) via ->
 209     D.le m[v] (D.add m[u] (D.Finite (weight u v)))
 210
 211
 212   let rec lemma inv2_path (m: distmap) (y z: vertex) (l:list vertex) : unit
 213     requires { inv2 m edges }
 214     requires { path y l z }
 215     ensures  { D.le m[z] (D.add m[y] (D.Finite (path_weight l z))) }
 216     variant  { length l }
 217   = match l with
 218     | Nil -> ()
 219     | Cons _ q ->
 220       let hd = match q with
 221         | Nil -> z
 222         | Cons h _ ->
 223           assert { path_weight l z = weight y h + path_weight q z };
 224           assert { D.le m[h] (D.add m[y] (D.Finite (weight y h))) };
 225           h
 226         end in
 227       inv2_path m hd z q
 228     end
 229
 230   (* key lemma for non-existence of a negative cycle
 231
 232      Proof: let us assume a negative cycle reachable from s, that is
 233          s --...--> x0 --w1--> x1 --w2--> x2 ... xn-1 --wn--> x0
 234        with w1+w2+...+wn < 0.
 235        Let di be the distance from s to xi as given by map m.
 236        By [inv2 m edges] we have di-1 + wi >= di for all i.
 237        Summing all such inequalities over the cycle, we get
 238             w1+w2+...+wn >= 0
 239        hence a contradiction.                                  Qed. *)
 240   lemma key_lemma_2:
 241      forall m: distmap. inv1 m (cardinal vertices) empty -> inv2 m edges ->
 242      forall v: vertex. not (negative_cycle v
 243        so exists l1. path s l1 v
 244        so exists l2. path v l2 v /\ path_weight l2 v < 0
 245        so D.le m[v] (D.add m[v] (D.Finite (path_weight l2 v)))
 246      )
 247
 248   let relax (m: distmap) (u v: vertex) (pass: int)
 249             (ghost via: fset (vertex, vertex))
 250     requires { 1 <= pass /\ mem (u, v) edges /\ not (mem (u, v) via) }
 251     requires { inv1 m pass via }
 252     ensures  { inv1 m pass (add (u, v) via) }
 253   = label I in
 254     let n = D.add m[u] (D.Finite (weight u v)) in
 255     if D.lt n m[v]
 256     then begin
 257       m[v] <- n;
 258       assert { match (m at I)[u] with
 259         | D.Infinite -> false
 260         | D.Finite w0 ->
 261           let w1 = w0 + weight u v in
 262           n = D.Finite w1
 263           && (exists l. path s l v /\ path_weight l v = w1
 264             by exists l2.
 265               path s l2 u /\ path_weight l2 u = w0 /\ l = l2 ++ Cons u Nil
 266           ) && (forall l. path s l v /\ length l < pass -> path_weight l v >= w1
 267             by match (m at I)[v] with
 268             | D.Infinite -> false
 269             | D.Finite w2 -> path_weight l v >= w2
 270             end
 271           ) && (forall z l. path s l z /\ length l < pass ->
 272             mem (z,v) (add (u,v) via) ->
 273             path_weight l z + weight z v >= w1
 274             by if z = u then path_weight l z >= w0
 275             else match (m at I)[v] with
 276               | D.Infinite -> false
 277               | D.Finite w2 -> path_weight l z + weight z v >= w2
 278               end
 279           )
 280         end
 281       }
 282     end else begin
 283       assert { forall l w1. path s l u /\ length l < pass /\ m[v] = D.Finite w1 ->
 284         path_weight l u + weight u v >= w1
 285         by match m[u] with
 286         | D.Infinite -> false
 287         | D.Finite w0 -> path_weight l u >= w0
 288         end
 289       }
 290     end
 291
 292   val get_edges (): S.set
 293     ensures { result = edges }
 294
 295   exception NegativeCycle
 296
 297   let bellman_ford ()
 298     ensures { forall v: vertex. mem v vertices ->
 299       match result[v] with
 300         | D.Finite n ->
 301             (exists l: list vertex. path s l v /\ path_weight l v = n) /\
 302             (forall l: list vertex. path s l v -> path_weight l v >= n
 303              by all_path_gt v n)
 304         | D.Infinite ->
 305             (forall l: list vertex. not (path s l v))
 306       end }
 307     raises { NegativeCycle -> exists v: vertex. negative_cycle v }
 308   = let m = initialize_single_source s in
 309     for i = 1 to nb_vertices - 1 do
 310       invariant { inv1 m i empty }
 311       let es = get_edges () in
 312       while not (S.is_empty es) do
 313         invariant { subset es.S.to_fset edges /\ inv1 m i (diff edges es.S.to_fset) }
 314         variant   { S.cardinal es }
 315         let ghost via = diff edges es.S.to_fset in
 316         let (u, v) = S.choose_and_remove es in
 317         relax m u v i via
 318       done;
 319       assert { inv1 m i edges }
 320     done;
 321     assert { inv1 m (cardinal vertices) empty };
 322     let es = get_edges () in
 323     while not (S.is_empty es) do
 324       invariant { subset es.S.to_fset edges /\ inv2 m (diff edges es.S.to_fset) }
 325       variant { S.cardinal es }
 326       let (u, v) = S.choose_and_remove es in
 327       if D.lt (D.add m[u] (D.Finite (weight u v))) m[v] then begin
 328         assert { match m[u], m[v] with
 329           | D.Infinite, _ -> false
 330           | D.Finite _, D.Infinite -> false
 331             by exists l2. path s l2 u
 332             so let l = l2 ++ Cons u Nil in path s l v
 333             so exists l. path s l v /\ length l < cardinal vertices
 334           | D.Finite wu, D.Finite wv ->
 335             (exists w. negative_cycle w)
 336             by
 337             all_path_gt v wv
 338             so exists l2. path s l2 u /\ path_weight l2 u = wu
 339             so let l = l2 ++ Cons u Nil in
 340               path s l v /\ path_weight l v < wv
 341           end
 342         };
 343         raise NegativeCycle
 344       end
 345     done;
 346     assert { inv2 m edges };
 347     assert { forall u. not (negative_cycle u) };
 348     m
 349
 350 end