Wiki Agenda Contact Version française

Bellman-Ford algorithm

Find all single-source shortest paths in a weighted directed graph, with detection of negative cycles.


Authors: Jean-Christophe Filliâtre / Yuto Takei

Topics: Graph Algorithms / Ghost code

Tools: Why3

see also the index (by topic, by tool, by reference, by year)



A proof of Bellman-Ford algorithm

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

theory Graph

  use export list.List
  use import list.Append
  use export list.Length
  use list.Mem
  use export int.Int
  use export set.Fset

  (* the graph is defined by a set of vertices and a set of edges *)
  type vertex
  constant vertices: set vertex
  constant edges: set (vertex, vertex)

  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 *)
  constant s: vertex
  axiom s_in_graph: mem s vertices

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

  (* 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.
  *)

  clone pigeon.Pigeonhole with type t = vertex

  lemma long_path_decomposition_pigeon1:
    forall l: list vertex, v: vertex.
    path s l v -> l <> Nil ->
    (forall v1: vertex. Mem.mem v1 (Cons v l) -> mem v1 vertices)

  lemma long_path_decomposition_pigeon2:
    forall l: list vertex, v: vertex.
    (forall v1: vertex. Mem.mem v1 (Cons v l) -> mem v1 vertices) ->
    length (Cons v l) > cardinal vertices ->
    (exists e: vertex, l1 l2 l3: list vertex.
    (Cons v l) = l1 ++ (Cons e (l2 ++ (Cons e l3))))

  lemma long_path_decomposition_pigeon3:
    forall l: list vertex, v: vertex.
    (exists e: vertex, l1 l2 l3: list vertex.
    (Cons v l) = l1 ++ (Cons e (l2 ++ (Cons e l3)))) ->
       (exists l1 l2: list vertex. l = l1 ++ Cons v l2)
    \/ (exists n: vertex, l1 l2 l3: list vertex.
          l = l1 ++ Cons n (l2 ++ Cons n l3))

  lemma long_path_decomposition:
    forall l: list vertex, v: vertex.
    path s l v -> length l >= cardinal vertices ->
       (exists l1 l2: list vertex. l = l1 ++ Cons v l2)
    \/ (exists n: vertex, l1 l2 l3: list vertex.
          l = l1 ++ Cons n (l2 ++ Cons n l3))

  lemma simple_path:
    forall v: vertex, l: list vertex. path s l v ->
    exists l': list vertex. path s l' v /\ length l' < cardinal vertices

  (* 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.
   *)
  lemma key_lemma_1:
    forall v: vertex, n: int.
    (* if any simple path has weight at least n *)
    (forall l: list vertex.
       path s l v -> length l < cardinal vertices -> path_weight l v >= n) ->
    (* and if there exists a shorter path *)
    (exists l: list vertex. path s l v /\ path_weight l v < n) ->
    (* then there exists a nagtive cycle *)
    exists u: vertex. negative_cycle u

end

module BellmanFord

  use import map.Map
  use map.Const
  use import Graph
  use int.IntInf as D

  use import ref.Ref
  use impset.Impset as S

  type distmap = map vertex D.t

  function initialize_single_source (s: vertex) : distmap =
    (Const.const D.Infinite)[s <- D.Finite 0]

  (* [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] *)
  predicate inv1 (m: distmap) (pass: int) (via: set (vertex, vertex)) =
    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

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

  (* 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 ->
     forall v: vertex. not (negative_cycle v)

  let relax (m: ref distmap) (u v: vertex) (pass: int)
            (ghost via: set (vertex, vertex))
    requires { 1 <= pass /\ mem (u, v) edges /\ not (mem (u, v) via) }
    requires { inv1 !m pass via }
    ensures  { inv1 !m pass (add (u, v) via) }
  = let n = D.add !m[u] (D.Finite (weight u v)) in
    if D.lt n !m[v] then m := !m[v <- n]

  exception NegativeCycle

  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) /\
            (forall l: list vertex. path s l v -> path_weight l v >= n)
        | D.Infinite ->
            (forall l: list vertex. not (path s l v))
      end }
    raises { NegativeCycle -> exists v: vertex. negative_cycle v }
  = let m = ref (initialize_single_source s) in
    for i = 1 to cardinal vertices - 1 do
      invariant { inv1 !m i empty }
      let es = S.create edges in
      while not (S.is_empty es) do
        invariant { subset !es edges /\ inv1 !m i (diff edges !es) }
        variant   { cardinal !es }
        let ghost via = diff edges !es in
        let (u, v) = S.pop es in
        relax m u v i via
      done;
      assert { inv1 !m i edges }
    done;
    assert { inv1 !m (cardinal vertices) empty };
    let es = S.create edges in
    while not (S.is_empty es) do
      invariant { subset !es edges /\ inv2 !m (diff edges !es) }
      variant { cardinal !es }
      let (u, v) = S.pop es in
      if D.lt (D.add !m[u] (D.Finite (weight u v))) !m[v] then begin
        raise NegativeCycle
      end
    done;
    assert { inv2 !m edges };
    !m

end

download ZIP archive

Why3 Proof Results for Project "bellman_ford"

Theory "bellman_ford.Graph": fully verified in 11.36 s

ObligationsAlt-Ergo (0.99.1)Coq (8.4pl6)
vertices_cardinal_pos0.01---
path_in_vertices---0.84
long_path_decomposition_pigeon1---1.50
long_path_decomposition_pigeon20.06---
long_path_decomposition_pigeon3---1.88
long_path_decomposition---1.65
simple_path---2.24
key_lemma_1---3.18

Theory "bellman_ford.BellmanFord": fully verified in 62.95 s

ObligationsAlt-Ergo (0.99.1)CVC3 (2.4.1)CVC4 (1.4)Coq (8.4pl6)Eprover (1.8-001)Spass (3.7)Vampire (0.6)Z3 (3.2)Z3 (4.3.2)
key_lemma_2---------6.78---------------
VC for relax---------------------------
split_goal_wp
  1. postcondition---------------------------
inline_goal
  1. postcondition---------------------------
split_goal_wp
  1. postcondition---------1.76---------------
2. postcondition---0.22---------------------
3. postcondition---0.34---------------------
4. postcondition0.140.23---------------------
5. postcondition---0.44---------------------
2. postcondition---------------------------
inline_goal
  1. postcondition---------------------------
split_goal_wp
  1. postcondition0.040.12---------------------
2. postcondition0.460.18---------------------
3. postcondition---0.31---------------------
4. postcondition0.070.08---------------------
5. postcondition---0.13---------------------
VC for bellman_ford---------------------------
split_goal_wp
  1. assertion---------------------------
inline_goal
  1. assertion---------------------------
split_goal_wp
  1. assertion------------0.112.660.16------
2. assertion0.03------------------------
3. assertion0.03------------------------
4. assertion0.03------------------------
5. assertion0.03------------------------
2. loop invariant init0.03------------------------
3. precondition0.01------------------------
4. exceptional postcondition---------2.17---------------
5. loop invariant preservation0.96------------------------
6. loop variant decrease0.02------------------------
7. assertion0.06------------------------
8. postcondition---------------------------
split_goal_wp
  1. postcondition0.060.10------------------0.03
2. postcondition---0.10---------------------
3. postcondition---0.04------------------0.04
9. loop invariant init---------------------------
inline_goal
  1. loop invariant init---------------------------
split_goal_wp
  1. loop invariant init------------0.12---0.16------
2. loop invariant init0.03------------------------
3. loop invariant init0.03------------------------
4. loop invariant init0.03------------------------
5. loop invariant init0.04------------------------
10. loop invariant init---------------------------
split_goal_wp
  1. VC for bellman_ford0.02------------------------
2. VC for bellman_ford0.13------------------------
11. precondition0.01------------------------
12. precondition0.02------------------------
13. precondition0.01------------------------
14. loop invariant preservation---------------------------
split_goal_wp
  1. VC for bellman_ford0.02------------------------
2. VC for bellman_ford---------------------------
inline_goal
  1. VC for bellman_ford---------------------------
split_goal_wp
  1. VC for bellman_ford0.480.35---------------------
2. VC for bellman_ford3.330.55---------------------
3. VC for bellman_ford---12.89---------------------
4. VC for bellman_ford1.790.13---------------------
5. VC for bellman_ford---7.93---------------------
15. loop variant decrease0.03------------------------
16. assertion---------------------------
inline_goal
  1. assertion4.02------------------------
17. loop invariant preservation---------------------------
inline_goal
  1. loop invariant preservation---------------------------
split_goal_wp
  1. loop invariant preservation0.16------------------------
2. loop invariant preservation---------2.31---------------
3. loop invariant preservation0.070.04---------------0.04---
4. loop invariant preservation---------1.82---------------
5. loop invariant preservation0.04------------------------
18. assertion0.02------------------------
19. loop invariant init0.06------------------------
20. precondition0.02------------------------
21. exceptional postcondition---------2.54---------------
22. loop invariant preservation---------------------------
split_goal_wp
  1. VC for bellman_ford0.02------------------------
2. VC for bellman_ford0.23------------------------
23. loop variant decrease0.02------------------------
24. assertion0.06------------------------
25. postcondition---------------------------
split_goal_wp
  1. postcondition0.110.13---------------0.03---
2. postcondition---------1.52---------------
3. postcondition0.820.14---------------0.03---