Figure 2. Bubble sort, the Bellman-Ford algorithm, and Dijkstra’s algorithm.

BubbleSort (A : array of reals)

1 for j := 1 to (|A| − 1);

2 do for i := 1 to (|A| − 1);

3 do if (A[i] > A[i + 1])

4 then t := A[i]; A[i] := A[i + 1]; A[i + 1] := t;

BellmanFord(G : array of reals, src : int)

1 …

2 for i := 1 to (|G| − 1)

3 do for each edge (v, w) of G

4 do if d[v] + G(v, w) < d[ w]

5 then d[ w] := d[v] + G(v, w)

Dijkstra(G : array of reals, src : int)

1 …

2 while W ≠ / 0

3 do choose edge (v, w)  W such that d[w] is minimal; 4 remove (v, w) from W;

5 if d[w] + G[w, v] < d[v]

6 then d[v] := d[ w] + G[ w, v]
of either “swapping A[i] and A[i + 1]” or “leaving A
unchanged.”
The core idea behind the rule Ite is to show that such a
divergence does not really matter, because at the program
states where arbitrarily small perturbations to the program
variables can “flip” the value of the guard b of the condi-
tional statement (let us call the set of such states the bound-
ary of b), the branches of the conditional are arbitrarily close
in behavior.

The rule Loop derives continuity judgments for while- loops. The idea here is to prove the body R of the loop continuous, then inductively argue that the entire loop is continuous too. In more detail, the rule derives a continuity judgment c  Cont(R, X, X), where c is a loop invariant— a property that is always true at the loop header—and X is a set of variables. Now consider any state s satisfying c. An arbitrarily small perturbation to this state leads to an arbitrarily small change in the value of each variable in X at the end of the first iteration, which only leads to an arbitrarily small change in the value of each variable in X at the end of the second iteration, and so on. Continuity follows.

Some subtleties need to be considered, however. An execution from a slightly perturbed state may terminate earlier or later than it would in the original execution. Even if the loop body is continuous, the extra iterations in either the modified or the original execution may cause the states at the loop exit to be very different. We rule out such scenarios by asserting a premise called synchronized termination. A loop “while b do R” fulfills this property with respect to a loop invariant c and a set of variables X, if B (b) ∧ c  R ≡x skip). Under this property, even if the loop reaches a state where a small perturbation can cause the loop to terminate earlier (similarly, later), the extra iterations in the original execution have no effect on the program state. We can ignore these iterations in our proof.

Second, even if the loop body is continuous in input xi and output xj for every xi, xj  X, an iteration may drastically change the value of program variables not in X. If there is a data flow from these variables to some variable in X, continuity will not hold. We rule out this scenario through an extra condition. Consider executions of P whose initial states satisfy a condition c. We call a set of variables X of P separable under c if the value of each z  X on termination of any such execution is independent of the initial values of variables not in X. We denote the fact that X is separable in this way by c  Sep(P, X).

To verify that P is continuous in input xi and output xj at state s, we derive a judgment b  Cont(P, {xi}, {xj}), where b is true at s. The correctness of the method follows from the following soundness theorem: Theorem 1. If the rules in Figure 1 can derive the judgment b  Cont(P, In, Out), then for all xi  In, xj  Out, and s such that b = true, P is continuous in input xi and output xj at s.

Example 5 (Warmup). Consider the program “if (x > 2) then x := x/2 else x := −5x + 11.” B(x > 2) equals (x = 2) and (x = 2)  (x := x/2) ≡{x} (x := −5x + 11). By Ite, the program is continuous in input x and output x.

Let us now use our rules on the algorithms in Figure 2.

Example 6 (Bubble Sort). Consider the implementation of Bubble Sort in Figure 2. (We assume it to be rewritten as a while- program in the obvious way.) Our goal is to derive the judgment true  Cont(BubbleSort, {A}, {A}).

Let X = {A, i, j}, and let us write R⟨p,q⟩ to denote the code fragment from line p to line q (both inclusive). Also, let us write c  Term(while b do R, X) as an abbreviation for B (b) ∧ c  (R ≡x skip).