Continuity and Robustness
of Programs

Abstract

Computer scientists have long believed that software is different from physical systems in one fundamental way: while the latter have continuous dynamics, the former do not. In this paper, we argue that notions of continuity from mathematical analysis are relevant and interesting even for software. First, we demonstrate that many everyday programs are continuous (i.e., arbitrarily small changes to their inputs only cause arbitrarily small changes to their outputs) or Lipschitz continuous (i.e., when their inputs change, their outputs change at most proportionally). Second, we give an mostly-automatic framework for verifying that a program is continuous or Lipschitz, showing that traditional, discrete approaches to proving programs correct can be extended to reason about these properties. An immediate application of our analysis is in reasoning about the robustness of programs that execute on uncertain inputs. In the longer run, it raises hopes for a toolkit for reasoning about programs that freely combines logical and analytical mathematics.

1. intRoDuCtion

It is accepted wisdom in computer science that the dynamics of software systems are inherently discontinuous, and that this fact makes them fundamentally different from physical systems. More than 25 years ago, Parnas15 attributed the difficulty of engineering reliable software to the fact that “the mathematical functions that describe the behavior of [software] systems are not continuous.” This meant that the traditional analytical calculus—the mathematics of choice when one is analyzing the dynamics of, say, fluids—did not fit the needs of software engineering too well. Logic, which can reason about discontinuous systems, was better suited to being the mathematics of programs.

In this paper, we argue that this wisdom is to be taken
with a grain of salt. First, many everyday programs are con-
tinuous in the same sense as in analysis—that is, arbitrarily
small changes to its inputs lead to arbitrarily small changes
to its outputs. Some of them are even Lipschitz continuous—
that is, perturbations to the program’s inputs lead to at
most proportional changes to its outputs. Second, we show
that analytic properties of programs are not at odds with
the classical, logical methods for program verification, giv-
ing a logic-based, mostly-automated method for formally
verifying that a program is continuous or Lipschitz contin-
uous. Among the immediate applications of this analysis
is reasoning about the robustness of programs that execute
under uncertainty. In the longer run, it raises hopes for a
unified theory of program analysis that marries logical and
analytical approaches.

Similar observations hold for many of the classic computa-
tions in computer science, for example, shortest path and
minimum spanning tree algorithms. Our program analysis
extends and automates methods from the traditional analyt-
ical calculus to prove the continuity or Lipschitz continuity
of such computations. For instance, to verify that a condi-
tional statement within a program is continuous, we gener-
alize the sort of insight that a high-school student uses to
prove the continuity of a piecewise function like
This paper is based on two previous works: “Continuity
Analysis of Programs,” by S. Chaudhuri, S. Gulwani, and
R. Lublinerman, published in POPL (2010), 57–70, and
“Proving Programs Robust,” by S. Chaudhuri, S. Gulwani,
R. Lublinerman, and S. Navidpour, published in FSE
(2011), 102–112.