Bellman-Ford algorithm
Find all single-source shortest paths in a weighted directed graph, with detection of negative cycles.
Auteurs: Jean-Christophe Filliâtre / Yuto Takei
Catégories: Graph Algorithms / Ghost code
Outils: 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 export list.Append 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 constant vertices: fset vertex constant edges: fset (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 *) val constant s: vertex ensures { mem result vertices } (* hence vertices is non empty *) lemma vertices_cardinal_pos: cardinal vertices > 0 val constant nb_vertices: int ensures { result = cardinal vertices } (* 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.ListAndSet with type t = vertex 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 lemma long_path_decomposition: 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) (* 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. *) 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 (* if any simple path has weight at least n *) requires { all_path_gt v n } (* and if there exists a shorter path *) 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: '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) end module ImpmapNoDom use map.Map use map.Const type key type t 'a = abstract { mutable contents: map key 'a } val function create (x: 'a): t 'a ensures { result.contents = const x } val function ([]) (m: t 'a) (k: key): 'a ensures { result = m.contents[k] } val ghost function ([<-]) (m: t 'a) (k: key) (v: 'a): t 'a ensures { result.contents = m.contents[k <- v] } val ([]<-) (m: t 'a) (k: key) (v: 'a): unit writes { m } ensures { m = (old m)[k <- v] } end module BellmanFord use Graph use int.IntInf as D use ref.Ref clone set.SetImp as S with type elt = (vertex, vertex) clone ImpmapNoDom with type key = vertex type distmap = ImpmapNoDom.t D.t let initialize_single_source (s: vertex): distmap ensures { result = (create D.Infinite)[s <- D.Finite 0] } = let m = create D.Infinite in m[s] <- D.Finite 0; m (* [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: fset (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: fset (vertex, vertex)) = forall u v: vertex. mem (u, v) via -> D.le m[v] (D.add m[u] (D.Finite (weight u v))) 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 (* 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 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))) ) let relax (m: distmap) (u v: vertex) (pass: int) (ghost via: fset (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) } = 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 val get_edges (): S.set ensures { result = edges } 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 by all_path_gt v n) | D.Infinite -> (forall l: list vertex. not (path s l v)) end } raises { NegativeCycle -> exists v: vertex. negative_cycle v } = 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 while not (S.is_empty es) do invariant { subset es.S.to_fset edges /\ inv1 m i (diff edges es.S.to_fset) } variant { S.cardinal es } let ghost via = diff edges es.S.to_fset in let (u, v) = S.choose_and_remove es in relax m u v i via done; assert { inv1 m i edges } done; assert { inv1 m (cardinal vertices) empty }; let es = get_edges () in while not (S.is_empty es) do invariant { subset es.S.to_fset edges /\ inv2 m (diff edges es.S.to_fset) } 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 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 }; raise NegativeCycle end done; assert { inv2 m edges }; assert { forall u. not (negative_cycle u) }; m end
download ZIP archive
Why3 Proof Results for Project "bellman_ford"
Theory "bellman_ford.Graph": fully verified
Obligations | Alt-Ergo 2.0.0 | Alt-Ergo 2.3.0 | Eprover 2.0 | ||
VC for s | --- | 0.00 | --- | ||
vertices_cardinal_pos | 0.00 | --- | --- | ||
path_in_vertices | 0.01 | --- | --- | ||
long_path_decomposition | --- | --- | --- | ||
split_goal_right | |||||
long_path_decomposition.0 | 0.17 | --- | --- | ||
long_path_decomposition.1 | 0.13 | --- | --- | ||
long_path_decomposition.2 | 0.17 | --- | --- | ||
long_path_decomposition.3 | 0.16 | --- | --- | ||
long_path_reduction | --- | --- | --- | ||
split_goal_right | |||||
long_path_reduction.0 | --- | --- | 0.04 | ||
long_path_reduction.1 | 0.01 | --- | --- | ||
long_path_reduction.2 | 0.01 | --- | --- | ||
VC for simple_path | 1.09 | --- | --- | ||
VC for key_lemma_1 | --- | --- | --- | ||
split_goal_right | |||||
assertion | --- | --- | --- | ||
split_goal_right | |||||
VC for key_lemma_1 | 0.01 | --- | --- | ||
VC for key_lemma_1 | 0.13 | --- | --- | ||
VC for key_lemma_1 | 0.33 | --- | --- | ||
VC for key_lemma_1 | 0.02 | --- | --- | ||
VC for key_lemma_1 | 0.04 | --- | --- | ||
VC for key_lemma_1 | 0.09 | --- | --- | ||
VC for key_lemma_1 | 0.09 | --- | --- | ||
VC for key_lemma_1 | 0.27 | --- | --- | ||
VC for key_lemma_1 | 0.02 | --- | --- | ||
variant decrease | 0.02 | --- | --- | ||
precondition | 0.01 | --- | --- | ||
precondition | 0.01 | --- | --- | ||
postcondition | 0.01 | --- | --- | ||
precondition | 0.02 | --- | --- | ||
precondition | 0.02 | --- | --- | ||
postcondition | 0.01 | --- | --- |
Theory "bellman_ford.BellmanFord": fully verified
Obligations | Alt-Ergo 2.0.0 | Alt-Ergo 2.2.0 | CVC4 1.6 | Eprover 2.0 | ||||||
VC for initialize_single_source | 0.01 | --- | --- | --- | ||||||
VC for inv2_path | --- | --- | --- | --- | ||||||
split_goal_right | ||||||||||
assertion | 0.02 | --- | --- | --- | ||||||
assertion | 0.08 | --- | --- | --- | ||||||
variant decrease | 0.03 | --- | --- | --- | ||||||
precondition | 0.01 | --- | --- | --- | ||||||
precondition | 0.22 | --- | --- | --- | ||||||
postcondition | --- | --- | --- | --- | ||||||
split_goal_right | ||||||||||
postcondition | 0.05 | --- | --- | --- | ||||||
postcondition | --- | --- | --- | --- | ||||||
split_goal_right | ||||||||||
postcondition | 0.09 | --- | --- | --- | ||||||
postcondition | 1.65 | --- | --- | --- | ||||||
key_lemma_2 | --- | --- | --- | --- | ||||||
split_goal_right | ||||||||||
key_lemma_2.0 | 0.79 | --- | --- | --- | ||||||
key_lemma_2.1 | 0.02 | --- | --- | --- | ||||||
key_lemma_2.2 | 0.02 | --- | --- | --- | ||||||
key_lemma_2.3 | 0.01 | --- | --- | --- | ||||||
VC for relax | --- | --- | --- | --- | ||||||
split_goal_right | ||||||||||
assertion | --- | --- | --- | --- | ||||||
split_goal_right | ||||||||||
VC for relax | 0.03 | --- | --- | --- | ||||||
VC for relax | 0.04 | --- | --- | --- | ||||||
VC for relax | --- | --- | --- | 2.02 | ||||||
VC for relax | 0.03 | --- | --- | --- | ||||||
VC for relax | 0.06 | --- | --- | --- | ||||||
VC for relax | 0.07 | --- | --- | --- | ||||||
VC for relax | 0.12 | --- | --- | --- | ||||||
VC for relax | 0.13 | --- | --- | --- | ||||||
VC for relax | 0.02 | --- | --- | --- | ||||||
VC for relax | 0.03 | --- | --- | --- | ||||||
VC for relax | 0.04 | --- | --- | --- | ||||||
VC for relax | 0.04 | --- | --- | --- | ||||||
postcondition | --- | --- | --- | --- | ||||||
introduce_premises | ||||||||||
postcondition | --- | --- | --- | --- | ||||||
inline_goal | ||||||||||
postcondition | --- | --- | --- | --- | ||||||
introduce_premises | ||||||||||
postcondition | --- | --- | --- | --- | ||||||
case (v=v1) | ||||||||||
true case (postcondition) | --- | --- | --- | --- | ||||||
split_goal_right | ||||||||||
VC for relax | 0.04 | --- | --- | --- | ||||||
VC for relax | 0.15 | --- | --- | --- | ||||||
VC for relax | 1.25 | --- | --- | --- | ||||||
VC for relax | 0.02 | --- | --- | --- | ||||||
VC for relax | 0.03 | --- | --- | --- | ||||||
false case (postcondition) | 0.36 | --- | --- | --- | ||||||
assertion | --- | --- | --- | --- | ||||||
split_goal_right | ||||||||||
assertion | 0.05 | --- | --- | --- | ||||||
assertion | 0.09 | --- | --- | --- | ||||||
VC for relax | 0.06 | --- | --- | --- | ||||||
postcondition | --- | --- | --- | --- | ||||||
introduce_premises | ||||||||||
postcondition | --- | --- | --- | --- | ||||||
inline_goal | ||||||||||
postcondition | --- | --- | --- | --- | ||||||
split_goal_right | ||||||||||
postcondition | 0.05 | --- | --- | --- | ||||||
postcondition | 0.09 | --- | --- | --- | ||||||
postcondition | 0.09 | --- | --- | --- | ||||||
postcondition | 0.04 | --- | --- | --- | ||||||
postcondition | 0.86 | --- | --- | --- | ||||||
VC for bellman_ford | --- | --- | --- | --- | ||||||
split_goal_right | ||||||||||
loop invariant init | --- | --- | --- | --- | ||||||
introduce_premises | ||||||||||
loop invariant init | --- | --- | --- | --- | ||||||
inline_goal | ||||||||||
loop invariant init | --- | --- | --- | --- | ||||||
split_goal_right | ||||||||||
loop invariant init | --- | --- | --- | 0.56 | ||||||
loop invariant init | 0.02 | --- | --- | --- | ||||||
loop invariant init | 0.07 | --- | --- | --- | ||||||
loop invariant init | 0.02 | --- | --- | --- | ||||||
loop invariant init | 0.06 | --- | --- | --- | ||||||
loop invariant init | 0.06 | --- | --- | --- | ||||||
precondition | 0.01 | --- | --- | --- | ||||||
precondition | 0.06 | --- | --- | --- | ||||||
precondition | 0.02 | --- | --- | --- | ||||||
loop variant decrease | 0.03 | --- | --- | --- | ||||||
loop invariant preservation | --- | --- | --- | --- | ||||||
split_goal_right | ||||||||||
VC for bellman_ford | --- | --- | 0.10 | --- | ||||||
VC for bellman_ford | --- | 1.26 | --- | --- | ||||||
assertion | 0.04 | --- | --- | --- | ||||||
loop invariant preservation | 0.34 | --- | --- | --- | ||||||
assertion | 0.02 | --- | --- | --- | ||||||
loop invariant init | 0.03 | --- | --- | --- | ||||||
precondition | 0.02 | --- | --- | --- | ||||||
assertion | --- | --- | --- | --- | ||||||
split_goal_right | ||||||||||
VC for bellman_ford | 0.06 | --- | --- | --- | ||||||
VC for bellman_ford | 0.07 | --- | --- | --- | ||||||
VC for bellman_ford | 0.04 | --- | --- | --- | ||||||
VC for bellman_ford | 0.32 | --- | --- | --- | ||||||
VC for bellman_ford | 0.05 | --- | --- | --- | ||||||
VC for bellman_ford | 0.04 | --- | --- | --- | ||||||
VC for bellman_ford | 0.20 | --- | --- | --- | ||||||
VC for bellman_ford | 0.14 | --- | --- | --- | ||||||
VC for bellman_ford | 0.08 | --- | --- | --- | ||||||
VC for bellman_ford | 0.21 | --- | --- | --- | ||||||
VC for bellman_ford | 0.04 | --- | --- | --- | ||||||
exceptional postcondition | 0.01 | --- | --- | --- | ||||||
loop variant decrease | 0.03 | --- | --- | --- | ||||||
loop invariant preservation | 0.27 | --- | --- | --- | ||||||
assertion | 0.06 | --- | --- | --- | ||||||
assertion | 0.04 | --- | --- | --- | ||||||
postcondition | --- | --- | --- | --- | ||||||
split_goal_right | ||||||||||
postcondition | 0.05 | --- | --- | --- | ||||||
postcondition | 0.46 | --- | --- | --- | ||||||
postcondition | 0.05 | --- | --- | --- | ||||||
VC for bellman_ford | 0.01 | --- | --- | --- | ||||||
out of loop bounds | 0.01 | --- | --- | --- |