论文标题
一种完整的循环验证方法和摘要的循环验证方法
A Complete Approach to Loop Verification with Invariants and Summaries
论文作者
论文摘要
不变性是验证循环正确性的主要方法。作为替代方案，循环合同明确地证明了基本归纳证明的前提和结论，有时可以更自然地捕获正确的条件。但是，尽管有这一优势，但第二种方法总体上很少受到关注，而本文的目的是将其从利基市场中脱颖而出。我们对循环合同理论的第一个全面论述，包括其完整性的特征。我们在标准算法上展示了它们相对优点的具体示例。此外，我们演示了两种方法之间的一种新颖的建设性翻译，从而将所选规范方法与验证后端解耦。
Invariants are the predominant approach to verify the correctness of loops. As an alternative, loop contracts, which make explicit the premise and conclusion of the underlying induction proof, can sometimes capture correctness conditions more naturally. But despite this advantage, the second approach receives little attention overall, and the goal of this paper is to lift it out of its niche. We give the first comprehensive exposition of the theory of loop contracts, including a characterization of its completeness. We show concrete examples on standard algorithms that showcase their relative merits. Moreover, we demonstrate a novel constructive translation between the two approaches, which decouples the chosen specification approach from the verification backend.
