It is easy to show that true  Sep(BubbleSort, X) and true  Sep(R⟨ 2, 4⟩, X). Each loop guard only involves discrete variables, hence we derive true  Term(BubbleSort, X) and true  Term(R⟨ 2, 4⟩, X).

Now consider R⟨ 3, 4⟩. As B(A[i] > A[i + 1]) equals (A[i] = A[i + 1]) and (A[i] = A[i + 1])  (skip ≡ X R⟨ 4, 4⟩), we have true  Cont(R⟨ 3, 4⟩, X, X), then true  Cont(R⟨ 2, 4⟩, X, X), and then true  Cont(BubbleSort, X, X). Now the In-Out rule derives the judgment we are after.

Example 7 (Bellman–Ford). Take the Bellman–Ford algorithm. On termination, d[u] contains the shortest path distance from the source node src to the node u. We want to prove that true  Cont(BellmanFord, {G}, {d}).

We use the symbols R⟨p, q⟩ and Term as before. Clearly, we have true  Sep(R⟨ 3, 5⟩, X) and true  Term(R⟨ 3, 5⟩, X), where X = {G, v, w}. The two branches of the conditional in Line 4 are X-equivalent at B(d[v] + G(v, w) < d[ w]), hence we have true =  Cont(R⟨ 4, 5⟩, X, X), and from this judgment, true  Cont(R⟨ 3, 5⟩, X, X). Similar arguments can be made about the outer loop. Now we can derive the fact true  Cont(BellmanFord, X, X); weakening, we get the judgment we seek.

Unfortunately, the rule Loop is not always enough for continuity proofs. Consider states s and s¢ of a continuous program P, where s¢ is obtained by slightly perturbing s. For Loop to apply, executions from s and s¢ must converge to close-by states at the end of each loop iteration. However, this need not be so. For example, think of Dijkstra’s algorithm. As a shortest path computation, this program is continuous in the input graph G and the output d—the array of shortest path distances. But let us look at its main loop in Figure 2.

Note that in any iteration, there may be several items w for which d[w] is minimal. But then, a slightly perturbed initial value of d may cause a loop iteration to choose a different w, leading to a drastic change in the value of d at the end of the iteration. Thus, individual iterations of this loop are not continuous, and we cannot apply Loop.

In prior work, 2 we gave a more powerful rule, called epoch induction, for proving the continuity of programs like the one above. The key insight here is that if we group some loop iterations together, then continuity becomes an inductive property of the groupings. For example, in Dijkstra’s algorithm, a “grouping” is a maximal set S of successive loop iterations that are tied on the initial value of d[ w]. Let s0 be the program state before the first iteration in S is executed. Owing to arbitrarily small perturbations to s0, we may execute iterations in S in a very different order. However, an iteration that ran after the iterations in S in the original execution will still run after the iterations in S. Moreover, for a fixed s0, the program state, once all iterations in S have been executed, is the same, no matter what order these iterations were executed in. Thus, a small perturbation cannot significantly change the state at the end of S, and the set of iterations S forms a continuous computation.

We have implemented the rules in Figure 1, as well as the epoch induction rule, in the form of a mostly-automatic program analysis. Given a program, the analysis iterates through its control points, assigning continuity

judgments to subprograms until convergence is reached. Auxiliary tasks such as checking the equivalence of two straight-line program fragments (needed by rule Ite) are performed automatically using the Z38 SMT-solver. Human intervention is expected in two forms. First, in applications of the epoch induction rule, we sometimes expect the programmer to write annotations that define appropriate “groupings” of iterations. Second, in case a complex loop invariant is needed for the proof (e.g., when one of the programs in a program equivalence query is a nested loop), the programmer is expected to supply it. There are heuristics and auxiliary tools that can be used to automate these steps, but our current system does not employ them.

Given the incompleteness of our proof rules, a natural empirical question for us was whether our system can verify the continuity of the continuous computing tasks described in Section 2. To answer this question, we chose several 13 continuous algorithms (including algorithms) over real and real array data types. Our system was able to verify the continuity of 11 of these algorithms, including the shortest path algorithms of Bellman-Ford, Dijkstra, and Floyd-Warshall; Merge Sort and Selection Sort in addition to Bubble Sort; and the minimum spanning tree algorithms of Prim and Kruskal. Among the algorithms we could not verify were Quick Sort. Please see Chaudhuri et al. 2 for more details.

3. 2. Verifying Lipschitz continuity

Now we extend the above verification framework to one for Lipschitz continuity. Let us fix variables xi and xj of the program P respectively as the input and the output variable. To start with, we assume that xi and xj are of continuous data types—reals or arrays of reals.

Let us define a control flow path of a program P as the sequence of assignment or skip-statements that P executes on some input (we omit a more formal definition). We note that since our arithmetic expressions are built from additions and multiplications, each control flow path of P encodes a continuous—in fact differentiable—function of the inputs. Now suppose we can show that each control flow path of P is a K-Lipschitz computation, for some K, in input xi and output xj. This does not mean that P is K-Lipschitz in this input and output: a perturbation to the initial value of xi can cause P to execute along a different control flow path, leading to a drastically different final state. However, if P is continuous and the above condition holds, then P is K-Lipschitz in input xi and output xj.

Our analysis exploits the above observation. To prove that P is K-Lipschitz in input xi and output xj, we establish that ( 1) P is continuous at all states in input xi and output xj and ( 2) each control flow path of P is K-Lipschitz in input xi and output xj. Of these, the first task is accomplished using the analysis from Section 3. 1. To accomplish the second task, we compute a data structure—a set of Lipschitz matrices—that contains upper bounds on the slopes of any computation that can be carried out in a control flow path of P.