使用后置条件推断循环不变式
Inferring Loop Invariants using Postconditions
摘要：
程序自动证明中的一个障碍是获得合适的循环不变量。循环的不变式是其后置条件（循环的目标，也称为其合同）的弱化形式;目前的工作利用这一观察，通过使用后置条件作为不变式推理的基础，使用各种算法，如“解耦”，证明在许多重要的算法中是有用的。由于这些抽象，该技术能够推断出各种各样的循环示例的不变量。我们提出的理论背后的技术，其实施（免费下载，目前依赖于微软研究院的布吉工具），并获得的结果。
英文摘要：
One of the obstacles in automatic program proving is to obtain suitable loop invariants. The invariant of a loop is a weakened form of its postcondition (the loop's goal, also known as its contract); the present work takes advantage of this observation by using the postcondition as the basis for invariant inference, using various heuristics such as "uncoupling" which prove useful in many important algorithms. Thanks to these heuristics, the technique is able to infer invariants for a large variety of loop examples. We present the theory behind the technique, its implementation (freely available for download and currently relying on Microsoft Research's Boogie tool), and the results obtained.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
