Intuitively, abs(x) is continuous because its two “pieces” x and −x are continuous, and because x and −x agree on values in the neighborhood of x = 0, the point where a small perturbation can cause abs(x) to switch from evaluating one piece to evaluating the other. Our analysis uses the same idea to prove that “if B then P1 else P2” is continuous: it inductively verifies that P1 and P2 are continuous, then checks, often automatically, that P1 and P2 become semantically equivalent at states where the value of B can flip on a small perturbation.

When operating on a program with loops, our analysis searches for an inductive proof of continuity. To prove that a continuous program is Lipschitz continuous, we inductively compute a collection of Lipschitz matrices that contain numerical bounds on the slopes of functions computed along different control paths of the program.

Of course, complete software systems are rarely continuous. However, verification technique like ours allows us to identify modules of a program that satisfy continuity properties. A benefit of this is that such modules are amenable to analysis by continuous methods. In the longer run, we can imagine a reasoning toolkit for programs that combines continuous analysis techniques, for example, numerical optimization or symbolic integration, and logical methods for analyzing code. Such a framework would expand the classical calculus to functions encoded as programs, a representation worthy of first-class treatment in an era where much of applied mathematics is computational.

A more immediate application of our framework is in the analysis of programs that execute on uncertain inputs, for example noisy sensor data or inexact scientific measurements. Unfortunately, traditional notions of functional correctness do not guarantee predictable program execution on uncertain inputs: a program may produce the correct output on each individual input, but even small amounts of noise in the input could change its output radically. Under uncertainty, traditional correctness properties must be supplemented by the property of robustness, which says that small perturbations to program’s inputs do not have much effect on the program’s output. Continuity and Lipschitz continuity can both serve as definitions of robustness, and our analysis can be used to prove that a program is robust.

The rest of the paper is organized as follows. In Section 2, we formally define continuity and Lipschitz continuity of programs and give a few examples of computations that satisfy these properties. In Section 3, we give a method for verifying a program’s continuity, and then extend it to an analysis for Lipschitz continuity. Related work is presented in Section 4; Section 5 concludes the paper with some discussion.

2. Continuity, LiPSChitz Continuity,
AnD RoBuStnESS

In this section, we define continuity2 and Lipschitz continuity3 of programs and show how they can be used to define robustness. First, however, we fix the programming language Imp whose programs we reason about.

Imp is a “core” language of imperative programs, meaning that it supports only the most central features of

imperative programming—assignments, branches, and loops. The language has two discrete data types—integers and arrays of integers—and two continuous data types— reals and arrays of reals. Usual arithmetic and comparisons on these types are supported. In conformance with the model of computation under which algorithms over reals are typically designed, our reals are infinite-precision, and elementary operations on them are assumed to be given by unit-time oracles.

Each data type in Imp is associated with a metric.a This metric is our notion of distance between values of a given type. For concreteness, we fix, for the rest of the paper, the following metrics for the Imp types:

• The integer and real types are associated with the Euclidean metric d(x, y) = |x − y|.

• The metric over arrays (of reals or integers) of the same length is the L∞-norm: d(A1, A2) = maxi{|A1[i] − A2[i]|}. Intuitively, an array changes by  when its size is kept fixed, but one or more of its items change by . We define d(A1, A2) = ∞ if A1 and A2 have different sizes.

The syntax of arithmetic expressions E, Boolean expressions B, and programs Prog is as follows: Here x is a typed variable, c is a typed constant, A is an array variable, i an integer variable or constant, + and · respectively represent addition and multiplication over scalars (reals or integers), and the Boolean operators are as usual. We assume an orthogonal type system that ensures that all expressions and assignments in our programs are well-typed. The set of variables appearing in P is denoted by Var (P) = {x1,…, xn}.

a Recall that a metric over a set S is a function d: S × S → R È {∞} such that for all x, y, z, we have ( 1) d(x, y) ≥ 0, with d(x, y) = 0 iff x = y; ( 2) d(x, y) = d(y, x); and ( 3) d(x, y) + d(y, z) ≥ d(x, z).