基于一种循环不变式构造方案的程序验证

摘要

大部分程序都要用到循环结构，如何有效地保证循环程序的正确性是程序正确性验证领域中重要的问题。目前针对循环程序的正确性验证存在着很多方案。其中，在程序中加入断言和不变式的证明方法是最为精确的一种。此方法通过数学上的证明对循环程序进行验证，保证程序的正确性。这种方法比传统的方法更准确，得出的结论也更具有说服力。但该方法在具体实施中存在着一些难点，主要表现在如何构造循环不变式。本文在综合考虑各种循环特征的基础上给出了一种循环不变式的构造方法。与传统的方法相比该方法可以更准确的反映程序运行的实际情况。