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: set vertex
  18   constant edges: set (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
 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 BellmanFord
 143
 144   use Graph
 145   use int.IntInf as D
 146   use ref.Ref
 147   clone impset.Impset as S with type elt = (vertex, vertex)
 148   clone impmap.ImpmapNoDom with type key = vertex
 149
 150   type distmap = ImpmapNoDom.t D.t
 151
 152   let initialize_single_source (s: vertex): distmap
 153     ensures { result = (create D.Infinite)[s <- D.Finite 0] }
 154   =
 155     let m = create D.Infinite in
 156     m[s] <- D.Finite 0;
 157     m
 158
 159   (* [inv1 m pass via] means that we already performed [pass-1] steps
 160      of the main loop, and, in step [pass], we already processed edges
 161      in [via] *)
 162   predicate inv1 (m: distmap) (pass: int) (via: set (vertex, vertex)) =
 163     forall v: vertex. mem v vertices ->
 164     match m[v] with
 165       | D.Finite n ->
 166         (* there exists a path of weight [n] *)
 167         (exists l: list vertex. path s l v /\ path_weight l v = n) /\
 168         (* there is no shorter path in less than [pass] steps *)
 169         (forall l: list vertex.
 170            path s l v -> length l < pass -> path_weight l v >= n) /\
 171         (* and no shorter path in i steps with last edge in [via] *)
 172         (forall u: vertex, l: list vertex.
 173            path s l u -> length l < pass -> mem (u,v) via ->
 174            path_weight l u + weight u v >= n)
 175       | D.Infinite ->
 176         (* any path has at least [pass] steps *)
 177         (forall l: list vertex. path s l v -> length l >= pass) /\
 178         (* [v] cannot be reached by [(u,v)] in [via] *)
 179         (forall u: vertex. mem (u,v) via -> (*m[u] = D.Infinite*)
 180           forall lu: list vertex. path s lu u -> length lu >= pass)
 181     end
 182
 183   predicate inv2 (m: distmap) (via: set (vertex, vertex)) =
 184     forall u v: vertex. mem (u, v) via ->
 185     D.le m[v] (D.add m[u] (D.Finite (weight u v)))
 186
 187
 188   let rec lemma inv2_path (m: distmap) (y z: vertex) (l:list vertex) : unit
 189     requires { inv2 m edges }
 190     requires { path y l z }
 191     ensures  { D.le m[z] (D.add m[y] (D.Finite (path_weight l z))) }
 192     variant  { length l }
 193   = match l with
 194     | Nil -> ()
 195     | Cons _ q ->
 196       let hd = match q with
 197         | Nil -> z
 198         | Cons h _ ->
 199           assert { path_weight l z = weight y h + path_weight q z };
 200           assert { D.le m[h] (D.add m[y] (D.Finite (weight y h))) };
 201           h
 202         end in
 203       inv2_path m hd z q
 204     end
 205
 206   (* key lemma for non-existence of a negative cycle
 207
 208      Proof: let us assume a negative cycle reachable from s, that is
 209          s --...--> x0 --w1--> x1 --w2--> x2 ... xn-1 --wn--> x0
 210        with w1+w2+...+wn < 0.
 211        Let di be the distance from s to xi as given by map m.
 212        By [inv2 m edges] we have di-1 + wi >= di for all i.
 213        Summing all such inequalities over the cycle, we get
 214             w1+w2+...+wn >= 0
 215        hence a contradiction.                                  Qed. *)
 216   lemma key_lemma_2:
 217      forall m: distmap. inv1 m (cardinal vertices) empty -> inv2 m edges ->
 218      forall v: vertex. not (negative_cycle v
 219        so exists l1. path s l1 v
 220        so exists l2. path v l2 v /\ path_weight l2 v < 0
 221        so D.le m[v] (D.add m[v] (D.Finite (path_weight l2 v)))
 222      )
 223
 224   let relax (m: distmap) (u v: vertex) (pass: int)
 225             (ghost via: set (vertex, vertex))
 226     requires { 1 <= pass /\ mem (u, v) edges /\ not (mem (u, v) via) }
 227     requires { inv1 m pass via }
 228     ensures  { inv1 m pass (add (u, v) via) }
 229   = label I in
 230     let n = D.add m[u] (D.Finite (weight u v)) in
 231     if D.lt n m[v]
 232     then begin
 233       m[v] <- n;
 234       assert { match (m at I)[u] with
 235         | D.Infinite -> false
 236         | D.Finite w0 ->
 237           let w1 = w0 + weight u v in
 238           n = D.Finite w1
 239           && (exists l. path s l v /\ path_weight l v = w1
 240             by exists l2.
 241               path s l2 u /\ path_weight l2 u = w0 /\ l = l2 ++ Cons u Nil
 242           ) && (forall l. path s l v /\ length l < pass -> path_weight l v >= w1
 243             by match (m at I)[v] with
 244             | D.Infinite -> false
 245             | D.Finite w2 -> path_weight l v >= w2
 246             end
 247           ) && (forall z l. path s l z /\ length l < pass ->
 248             mem (z,v) (add (u,v) via) ->
 249             path_weight l z + weight z v >= w1
 250             by if z = u then path_weight l z >= w0
 251             else match (m at I)[v] with
 252               | D.Infinite -> false
 253               | D.Finite w2 -> path_weight l z + weight z v >= w2
 254               end
 255           )
 256         end
 257       }
 258     end else begin
 259       assert { forall l w1. path s l u /\ length l < pass /\ m[v] = D.Finite w1 ->
 260         path_weight l u + weight u v >= w1
 261         by match m[u] with
 262         | D.Infinite -> false
 263         | D.Finite w0 -> path_weight l u >= w0
 264         end
 265       }
 266     end
 267
 268   val get_edges (): S.t
 269     ensures { result.S.contents = edges }
 270
 271   exception NegativeCycle
 272
 273   let bellman_ford ()
 274     ensures { forall v: vertex. mem v vertices ->
 275       match result[v] with
 276         | D.Finite n ->
 277             (exists l: list vertex. path s l v /\ path_weight l v = n) /\
 278             (forall l: list vertex. path s l v -> path_weight l v >= n
 279              by all_path_gt v n)
 280         | D.Infinite ->
 281             (forall l: list vertex. not (path s l v))
 282       end }
 283     raises { NegativeCycle -> exists v: vertex. negative_cycle v }
 284   = let m = initialize_single_source s in
 285     for i = 1 to nb_vertices - 1 do
 286       invariant { inv1 m i empty }
 287       let es = get_edges () in
 288       while not (S.is_empty es) do
 289         invariant { subset es.S.contents edges /\ inv1 m i (diff edges es.S.contents) }
 290         variant   { S.cardinal es }
 291         let ghost via = diff edges es.S.contents in
 292         let (u, v) = S.choose_and_remove es in
 293         relax m u v i via
 294       done;
 295       assert { inv1 m i edges }
 296     done;
 297     assert { inv1 m (cardinal vertices) empty };
 298     let es = get_edges () in
 299     while not (S.is_empty es) do
 300       invariant { subset es.S.contents edges /\ inv2 m (diff edges es.S.contents) }
 301       variant { S.cardinal es }
 302       let (u, v) = S.choose_and_remove es in
 303       if D.lt (D.add m[u] (D.Finite (weight u v))) m[v] then begin
 304         assert { match m[u], m[v] with
 305           | D.Infinite, _ -> false
 306           | D.Finite _, D.Infinite -> false
 307             by exists l2. path s l2 u
 308             so let l = l2 ++ Cons u Nil in path s l v
 309             so exists l. path s l v /\ length l < cardinal vertices
 310           | D.Finite wu, D.Finite wv ->
 311             (exists w. negative_cycle w)
 312             by
 313             all_path_gt v wv
 314             so exists l2. path s l2 u /\ path_weight l2 u = wu
 315             so let l = l2 ++ Cons u Nil in
 316               path s l v /\ path_weight l v < wv
 317           end
 318         };
 319         raise NegativeCycle
 320       end
 321     done;
 322     assert { inv2 m edges };
 323     assert { forall u. not (negative_cycle u) };
 324     m
 325
 326 end