Great advances in program analysis would be enabled if it were possible to derive the function of a program from inputs to outputs (or from initial states to final states, depending on how we model program semantics). Efforts to do so have always stalled against the difficulty to derive the function of loops; the expedient solution to capture the function of loops by unrolling them an arbitrary number of iterations is clearly inadequate. In this paper, we propose a relations-based method to derive the function of a C-like program, including programs that have loops nested to an arbitrary level. To capture the semantics of loops, we use the concept of invariant relation.

翻译：如果能够从输入到输出（或从初始状态到最终状态，具体取决于我们如何建模程序语义）推导出程序的功能，那么程序分析将取得重大进展。然而，这种尝试总是因为难以推导循环的功能而受阻；通过任意次迭代展开循环来获取其功能的权宜之计显然是不够的。在本文中，我们提出一种基于关系的方法，用于推导类C语言程序（包括包含任意层次嵌套循环的程序）的功能。为捕捉循环的语义，我们引入了不变关系的概念。