∀i, j: J(i, j) = 0 ∨ J(i, j) ≥ 1. Note that in the course of a proof, we can weaken any Lipschitz matrix for the loop body to a matrix J of this form.

We can prove the following soundness theorem: Theorem 2. Let P be continuous in input xi and output xj . If the rules in Figure 3 derive the judgment P : {J}, then P is J(j, i)- Lipschitz in input xi and output xj.

Example 8 (Warmup). Recall the program “if (x > 2) then x := x/2 else x := −5x + 11” from Example 5 (x is a real). Our rules can associate the left branch with a single Lipschitz matrix containing a single entry , and the right branch with a single matrix containing a single entry 5. Given the continuity of the program, we conclude that the program is 5-Lipschitz in input x and output x.

Example 9 (Bubble Sort). Consider the Bubble Sort algorithm (Figure 2) once again, and as before, let R⟨p,q⟩ denote the code fragment from line p to line q. Let us set x0 to be A and x1 to be t.

Now, let . From the rules in Figure 3, we can derive (t := A[i]) : { J}, (A[i ] := A[i + 1]) : {I}, and (A[i + 1] := t) : {J, I}.

Carrying out the requisite matrix multiplications, we get R⟨ 4, 4⟩ : {J}. Using the rule Ite, we have R⟨ 3, 4⟩ : {I, J}. Now, it is easy to show that R⟨ 3, 4⟩ gets executed N times, where N is the size of A. From this we have R⟨ 2, 4⟩ : {I, J}N. Given that J2 = IJ = JI = J, this is equivalent to the judgment R⟨ 2, 4⟩ : {I, J}. From this, we derive BubbleSort : {J, I}. Given the proof of continuity carried out in Example 1, Bubble Sort is 1-Lipschitz in input A and output A.

Intuitively, the reason why Bubble Sort is so robust is that here, ( 1) there is no data flow from program points where arithmetic operations are carried out to points where values are assigned to the output variable and ( 2) continuity holds everywhere. In fact, one can formally prove that any program that meets the above two criteria is 1-Lipschitz. However, we do not develop this argument here.

Example 10 (Bellman–Ford; Dijkstra). Let us consider the Bellman–Ford algorithm (Figure 2) once again, and let x0 be G and x1 be d. Consider line 5 (i.e., the program R⟨ 5, 5⟩); our rules can assign to this program the Lipschitz matrix J, where Using the rule for loops, we have R⟨ 3, 5⟩ : {JN}, where N is the number of edges in G, and then BellmanFord : {JN2}. But note that Combing the above with the continuity proof in Example 7, we decide that the Bellman–Ford algorithm is N2-Lipschitz in input G and output d.

the same reasoning as above, we assign to the main loop of the algorithm the single Lipschitz matrix J. Applying the Loop rule, we derive Given that the algorithm is continuous in input G and output d, it is N-Lipschitz in input G and output d.

4. RELAtED WoRk

So far as we know, we were the first2 to propose a framework for continuity analysis of programs. Before us, Hamlet12 advocated notions of continuity of software; however, he concluded that “it is not possible in practice to mechanically test for continuity” in the presence of