bellman_ford.mlw 11.9 KB
Newer Older
1 2 3 4 5 6 7 8

(** {1 A proof of Bellman-Ford algorithm}

   By Yuto Takei (University of Tokyo, Japan)
   and Jean-Christophe Filliâtre (CNRS, France). *)

theory Graph

9
  use export list.List
10
  use export list.Append
11 12 13 14 15 16
  use export list.Length
  use export int.Int
  use export set.Fset

  (* the graph is defined by a set of vertices and a set of edges *)
  type vertex
17 18
  constant vertices: fset vertex
  constant edges: fset (vertex, vertex)
19 20 21 22 23 24 25 26 27

  predicate edge (x y: vertex) = mem (x,y) edges

  (* edges are well-formed *)
  axiom edges_def:
    forall x y: vertex.
    mem (x, y) edges -> mem x vertices /\ mem y vertices

  (* a single source vertex s is given *)
28 29
  val constant s: vertex
    ensures { mem result vertices }
30 31 32 33

  (* hence vertices is non empty *)
  lemma vertices_cardinal_pos: cardinal vertices > 0

34 35 36
  val constant nb_vertices: int
    ensures { result = cardinal vertices }

37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61
  (* paths *)
  clone export graph.IntPathWeight
     with type vertex = vertex, predicate edge = edge

  lemma path_in_vertices:
    forall v1 v2: vertex, l: list vertex.
    mem v1 vertices -> path v1 l v2 -> mem v2 vertices

  (* A key idea behind Bellman-Ford's correctness is that of simple path:
     if there is a path from s to v, there is a path with less than
     |V| edges. We formulate this in a slightly more precise way: if there
     a path from s to v with at least |V| edges, then there must be a duplicate
     vertex along this path. There is a subtlety here: since the last vertex
     of a path is not part of the vertex list, we distinguish the case where
     the duplicate vertex is the final vertex v.

     Proof: Assume [path s l v] with length l >= |V|.
       Consider the function f mapping i in {0..|V|} to the i-th element
       of the list l ++ [v]. Since all elements of the
       path (those in l and v) belong to V, then by the pigeon hole principle,
       f cannot be injective from 0..|V| to V. Thus there exist two distinct
       i and j in 0..|V| such that f(i)=f(j), which means that
              l ++ [v] = l1 ++ [u] ++ l2 ++ [u] ++ l3
       Two cases depending on l3=[] (and thus u=v) conclude the proof. Qed.
  *)
62

63
  clone pigeon.ListAndSet with type t = vertex
64

65 66 67 68
  predicate cyc_decomp (v: vertex) (l: list vertex)
                       (vi: vertex) (l1 l2 l3: list vertex) =
    l = l1 ++ l2 ++ l3 /\ length l2 > 0 /\
    path s l1 vi /\ path vi l2 vi /\ path vi l3 v
69

70
  lemma long_path_decomposition:
71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93
    forall l v. path s l v /\ length l >= cardinal vertices ->
      (exists vi l1 l2 l3. cyc_decomp v l vi l1 l2 l3)
      by exists n l1 l2 l3. Cons v l = l1 ++ Cons n (l2 ++ Cons n l3)
      so match l1 with
        | Nil -> cyc_decomp v l v l2 (Cons n l3) Nil
        | Cons v l1 -> cyc_decomp v l n l1 (Cons n l2) (Cons n l3)
        end

  lemma long_path_reduction:
    forall l v. path s l v /\ length l >= cardinal vertices ->
      exists l'. path s l' v /\ length l' < length l
      by exists vi l1 l2 l3. cyc_decomp v l vi l1 l2 l3 /\ l' = l1 ++ l3

  let lemma simple_path (v: vertex) (l: list vertex) : unit
    requires { path s l v }
    ensures  { exists l'. path s l' v /\ length l' < cardinal vertices }
  = let rec aux (n: int) : unit
      ensures { forall l. length l <= n /\ path s l v ->
          exists l'. path s l' v /\ length l' < cardinal vertices }
      variant { n }
    = if n > 0 then aux (n-1)
    in
    aux (length l)
94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111

  (* negative cycle [v] -> [v] reachable from [s] *)
  predicate negative_cycle (v: vertex) =
    mem v vertices /\
    (exists l1: list vertex. path s l1 v) /\
    (exists l2: list vertex. path v l2 v /\ path_weight l2 v < 0)

  (* key lemma for existence of a negative cycle

     Proof: by induction on the (list) length of the shorter path l
       If length l < cardinal vertices, then it contradicts hypothesis 1
       thus length l >= cardinal vertices and thus the path contains a cycle
             s ----> n ----> n ----> v
       If the weight of the cycle n--->n is negative, we are done.
       Otherwise, we can remove this cycle from the path and we get
       an even shorter path, with a stricltly shorter (list) length,
       thus we can apply the induction hypothesis.                     Qed.
   *)
112 113 114 115
  predicate all_path_gt (v: vertex) (n: int) =
    forall l. path s l v /\ length l < cardinal vertices -> path_weight l v >= n

  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 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138
    requires { path s l v /\ path_weight l v < n }
    (* then there exists a negative cycle. *)
    ensures  { exists u. negative_cycle u }
  = let rec aux (m: int) : 'a
      requires { forall u. not negative_cycle u }
      requires { exists l. path s l v /\ path_weight l v < n /\ length l <= m }
      ensures  { false }
      variant  { m }
    = assert { (exists l'. path s l' v /\ path_weight l' v < n /\ length l' < m)
        by exists l. path s l v /\ path_weight l v < n /\ length l <= m
        so exists vi l1 l2 l3. cyc_decomp v l vi l1 l2 l3
        so let res = l1 ++ l3 in
          path s res v /\ length res < length l /\ path_weight res v < n
          by path_weight l v =
            path_weight l1 vi + path_weight l2 vi + path_weight l3 v
          so path_weight l2 vi >= 0 by not negative_cycle vi
      };
      aux (m-1)
    in
    if pure { forall u. not negative_cycle u } then aux (length l)
139 140 141 142 143

end

module BellmanFord

144
  use Graph
145
  use int.IntInf as D
146
  use ref.Ref
147
  clone set.SetImp 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 153 154
  let initialize_single_source (s: vertex): distmap
    ensures { result = (create D.Infinite)[s <- D.Finite 0] }
  =
155 156 157
    let m = create D.Infinite in
    m[s] <- D.Finite 0;
    m
158 159 160 161

  (* [inv1 m pass via] means that we already performed [pass-1] steps
     of the main loop, and, in step [pass], we already processed edges
     in [via] *)
162
  predicate inv1 (m: distmap) (pass: int) (via: fset (vertex, vertex)) =
163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182
    forall v: vertex. mem v vertices ->
    match m[v] with
      | D.Finite n ->
        (* there exists a path of weight [n] *)
        (exists l: list vertex. path s l v /\ path_weight l v = n) /\
        (* there is no shorter path in less than [pass] steps *)
        (forall l: list vertex.
           path s l v -> length l < pass -> path_weight l v >= n) /\
        (* and no shorter path in i steps with last edge in [via] *)
        (forall u: vertex, l: list vertex.
           path s l u -> length l < pass -> mem (u,v) via ->
           path_weight l u + weight u v >= n)
      | D.Infinite ->
        (* any path has at least [pass] steps *)
        (forall l: list vertex. path s l v -> length l >= pass) /\
        (* [v] cannot be reached by [(u,v)] in [via] *)
        (forall u: vertex. mem (u,v) via -> (*m[u] = D.Infinite*)
          forall lu: list vertex. path s lu u -> length lu >= pass)
    end

183
  predicate inv2 (m: distmap) (via: fset (vertex, vertex)) =
184 185 186
    forall u v: vertex. mem (u, v) via ->
    D.le m[v] (D.add m[u] (D.Finite (weight u v)))

187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205

  let rec lemma inv2_path (m: distmap) (y z: vertex) (l:list vertex) : unit
    requires { inv2 m edges }
    requires { path y l z }
    ensures  { D.le m[z] (D.add m[y] (D.Finite (path_weight l z))) }
    variant  { length l }
  = match l with
    | Nil -> ()
    | Cons _ q ->
      let hd = match q with
        | Nil -> z
        | Cons h _ ->
          assert { path_weight l z = weight y h + path_weight q z };
          assert { D.le m[h] (D.add m[y] (D.Finite (weight y h))) };
          h
        end in
      inv2_path m hd z q
    end

206 207 208 209 210 211 212 213 214 215 216 217
  (* key lemma for non-existence of a negative cycle

     Proof: let us assume a negative cycle reachable from s, that is
         s --...--> x0 --w1--> x1 --w2--> x2 ... xn-1 --wn--> x0
       with w1+w2+...+wn < 0.
       Let di be the distance from s to xi as given by map m.
       By [inv2 m edges] we have di-1 + wi >= di for all i.
       Summing all such inequalities over the cycle, we get
            w1+w2+...+wn >= 0
       hence a contradiction.                                  Qed. *)
  lemma key_lemma_2:
     forall m: distmap. inv1 m (cardinal vertices) empty -> inv2 m edges ->
218 219 220 221 222
     forall v: vertex. not (negative_cycle v
       so exists l1. path s l1 v
       so exists l2. path v l2 v /\ path_weight l2 v < 0
       so D.le m[v] (D.add m[v] (D.Finite (path_weight l2 v)))
     )
223

224
  let relax (m: distmap) (u v: vertex) (pass: int)
225
            (ghost via: fset (vertex, vertex))
226
    requires { 1 <= pass /\ mem (u, v) edges /\ not (mem (u, v) via) }
227 228
    requires { inv1 m pass via }
    ensures  { inv1 m pass (add (u, v) via) }
229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266
  = label I in
    let n = D.add m[u] (D.Finite (weight u v)) in
    if D.lt n m[v]
    then begin
      m[v] <- n;
      assert { match (m at I)[u] with
        | D.Infinite -> false
        | D.Finite w0 ->
          let w1 = w0 + weight u v in
          n = D.Finite w1
          && (exists l. path s l v /\ path_weight l v = w1
            by exists l2.
              path s l2 u /\ path_weight l2 u = w0 /\ l = l2 ++ Cons u Nil
          ) && (forall l. path s l v /\ length l < pass -> path_weight l v >= w1
            by match (m at I)[v] with
            | D.Infinite -> false
            | D.Finite w2 -> path_weight l v >= w2
            end
          ) && (forall z l. path s l z /\ length l < pass ->
            mem (z,v) (add (u,v) via) ->
            path_weight l z + weight z v >= w1
            by if z = u then path_weight l z >= w0
            else match (m at I)[v] with
              | D.Infinite -> false
              | D.Finite w2 -> path_weight l z + weight z v >= w2
              end
          )
        end
      }
    end else begin
      assert { forall l w1. path s l u /\ length l < pass /\ m[v] = D.Finite w1 ->
        path_weight l u + weight u v >= w1
        by match m[u] with
        | D.Infinite -> false
        | D.Finite w0 -> path_weight l u >= w0
        end
      }
    end
267

268 269
  val get_edges (): S.set
    ensures { result = edges }
270 271 272

  exception NegativeCycle

273 274 275 276 277
  let bellman_ford ()
    ensures { forall v: vertex. mem v vertices ->
      match result[v] with
        | D.Finite n ->
            (exists l: list vertex. path s l v /\ path_weight l v = n) /\
278 279
            (forall l: list vertex. path s l v -> path_weight l v >= n
             by all_path_gt v n)
280 281 282 283
        | D.Infinite ->
            (forall l: list vertex. not (path s l v))
      end }
    raises { NegativeCycle -> exists v: vertex. negative_cycle v }
284 285 286 287
  = let m = initialize_single_source s in
    for i = 1 to nb_vertices - 1 do
      invariant { inv1 m i empty }
      let es = get_edges () in
288
      while not (S.is_empty es) do
289
        invariant { subset es.S.to_fset edges /\ inv1 m i (diff edges es.S.to_fset) }
290
        variant   { S.cardinal es }
291
        let ghost via = diff edges es.S.to_fset in
292
        let (u, v) = S.choose_and_remove es in
293 294
        relax m u v i via
      done;
295
      assert { inv1 m i edges }
296
    done;
297 298
    assert { inv1 m (cardinal vertices) empty };
    let es = get_edges () in
299
    while not (S.is_empty es) do
300
      invariant { subset es.S.to_fset edges /\ inv2 m (diff edges es.S.to_fset) }
301 302 303
      variant { S.cardinal es }
      let (u, v) = S.choose_and_remove es in
      if D.lt (D.add m[u] (D.Finite (weight u v))) m[v] then begin
304 305 306 307 308 309 310 311 312 313 314 315 316 317 318
        assert { match m[u], m[v] with
          | D.Infinite, _ -> false
          | D.Finite _, D.Infinite -> false
            by exists l2. path s l2 u
            so let l = l2 ++ Cons u Nil in path s l v
            so exists l. path s l v /\ length l < cardinal vertices
          | D.Finite wu, D.Finite wv ->
            (exists w. negative_cycle w)
            by
            all_path_gt v wv
            so exists l2. path s l2 u /\ path_weight l2 u = wu
            so let l = l2 ++ Cons u Nil in
              path s l v /\ path_weight l v < wv
          end
        };
319 320 321
        raise NegativeCycle
      end
    done;
322
    assert { inv2 m edges };
323
    assert { forall u. not (negative_cycle u) };
324
    m
325 326

end