this problem is discontinuous with respect to the input c and also with respect to the input Budget. At the same time, Knap is N-Lipschitz with respect to the input v: if the value of each item changes by ±, the value of totv can change by ±N.

Continuity and Lipschitz continuity can be used as definitions of robustness, a property that ensures that a program behaves predictably on uncertain inputs. Uncertainty, in this context, can be modeled by either nondeterminism (the value of x has a margin of error ±) or a probability distribution. For example, a robust embedded controller does not change its control decisions abruptly because of uncertainty in its sensor-derived inputs. The statistics computed by a robust scientific program are not much affected by measurement errors in the input dataset.

Robustness has benefits even in contexts where a program’s relationship with uncertainty is not adversarial. The input space of a robust program does not have isolated “peaks”—that is, points where the program output is very different from outputs on close-by inputs. Therefore, we are more likely to cover a program’s behaviors using random tests if the program is robust. Also, robust computations are more amenable to randomized and approximate program transformations20 that explore trade-offs between a program’s quality of results and resource consumption. Transformations of this sort can be seen to deliberately introduce uncertainty into a program’s operational semantics. If the program is robust, then this extra uncertainty does not significantly affect its observable behavior, hence such a transformation is “safer” to perform. More details are available in our conference paper on robustness analysis. 3

Now, if a program is Lipschitz, then we can give quantitative upper bounds on the change to its behavior due to uncertainty in its inputs, and further, this bound is small if the inputs are only slightly uncertain. Consequently, Lipschitz continuity is a rather strong robustness property. Continuity is a weaker definition of robustness—a program computing ex is continuous, even though it hugely amplifies errors in its inputs. Nonetheless, it captures freedom from a common class of robustness violations: those where uncertainty in the inputs alters a program’s control flow, and this change leads to a significant change in the program’s output.

3. PRoGRAM VERiFiCAtion

Now we present our automated framework for proving a program continuous2 or Lipschitz. 3 Our analysis is sound— that is, a program proven continuous or Lipschitz by our analysis is indeed continuous. However, as the analysis targets a Turing-complete language, it is incomplete—for example, a program may be continuous even if the analysis does not deem it so.

3. 1. Verifying continuity

First we show how to verify the continuity of an Imp program. We use as running examples three of the most well-known algorithms of computing: Bubble Sort, the Bellman–Ford shortest path algorithm, and Dijkstra’s shortest path algorithm (Figure 2). As mentioned in Example 1, a program is always continuous in input variables of discrete types.

Therefore, to make the problem more interesting, we assume that the input to Bubble Sort is an array of reals. As before, we model graphs by arrays of reals where each item represents the weight of an edge.

Given a program P, our task is to derive a syntactic continuity judgment for P, defined as a term b  Cont(P, In, Out), where b is a Boolean formula over Var, and In and Out are sets of variables of P. Such a judgment is read as “For each xi  In and xj  Out and each state s where b is true, P is continuous in input xi and output xj at s.” We break down this task into the task of deriving judgments b  Cont(P¢, In, Out) for programs P¢ that are syntactic substructures of P. For example, if P is of the form “if b then P1 else P2,” then we recursively derive continuity judgments for P1 and P2.

Continuity judgments are derived using a set of syntactic proof rules—the rules can be converted in a standard way into an automated program analysis that iteratively assigns continuity judgments to subprograms. Figure 1 shows the most important of our rules; for the full set, see the original reference. 2 To understand the syntax of the rules, consider the rule Base. This rule derives a conclusion b  Cont(P, In, Out), where b, In, and Out are arbitrary, from the premise that P is either “skip” or an assignment.

The rule Sequence addresses sequential composition of programs, generalizing the fact that the composition of two continuous functions is continuous. One of the premises of this rule is a Hoare triple of the form {b1}P{b2}. This is to be read as “For any state s that satisfies b1, P (s) satisfies b2. (A standard program verifier can be used to verify this premise.) The rule In-Out allows us to restrict or generalize the set of input and output variables with respect to which a continuity judgment is made.

The next rule—Ite—handles conditional statements, and is perhaps the most interesting of our rules. In a conditional branch, a small perturbation to the input variables can cause control to flow along a different branch, leading to a syntactically divergent behavior. For instance, this happens in Lines 3–4 in the Bubble Sort algorithm in Figure 2— perturbations to items in A can lead to either behaviors