Users of program analyses expect that results change predictably in response to changes in their programs, but many analyses fail to provide such robustness. This paper introduces a theoretical framework that provides a unified language to articulate robustness properties. By modeling programs and their properties as objects in a category, diverse notions of robustness-from variable renaming to semantic refinement and structural transformation-can be characterized as structure-preserving functors. Beyond formulating the meaning of robustness, this paper provides methods for achieving it. The first is a general recipe for designing robust analyses, by lifting a sound and robust analysis from a restricted (sub-Turing) model of computation to a sound and robust analysis for general programs. This recipe demystifies the design of several existing loop summarization and termination analyses by showing they are instantiations of this general recipe, and furthermore elucidates their robustness properties. The second is a characterization of a sense in which an algebraic program analysis is robust, provided that it is comprised of robust operators. In particular, we show that such analyses behave predictably under common refactoring patterns, such as variable renaming and loop unrolling.

翻译：程序分析的用户期望结果能够随着程序的变化而可预测地改变，但许多分析未能提供这种健壮性。本文引入了一个理论框架，该框架提供了一种统一的语言来描述健壮性属性。通过将程序及其属性建模为范畴中的对象，从变量重命名到语义精化及结构变换的各种健壮性概念，都可以被刻画为保持结构的函子。除了阐述健壮性的含义，本文还提供了实现健壮性的方法。第一种方法是一种设计健壮分析的通则，通过将受限（亚图灵）计算模型上的可靠且健壮的分析提升为针对通用程序的可靠且健壮的分析。该通则揭示了若干现有循环摘要与终止分析的设计思路，表明它们都是这一通则的实例，并进一步阐明了它们的健壮性属性。第二种方法刻画了这样一种意义：一种代数程序分析（只要它由健壮的算子组成）便是健壮的。特别地，我们证明了此类分析在诸如变量重命名和循环展开之类的常见重构模式下的行为是可预测的。