论文部分内容阅读
Ｆｌｏｙｄ的循环不变式断言法是部分正确性证明的常用方法之一，但循环不变式断言的构造是比较困难的，而染色网（ＣＰＮ）的位置不变量是可求出的．本文通过用ＣＰＮ描述程序算法，引出了一种拓广的位置不变式的定义，此定义允许不变式是非线性的，以及计算不变式的一个充分条件，并且讨论了上述两种不变式之间的联系，为构造一算法的循环不变式断言提供了一种新的方法．
Floyd’s cyclic invariant assertion method is one of the commonly used methods to prove partial correctness. However, the construction of cyclic invariant assertions is difficult, while the position invariants of the CPN can be obtained. In this paper, by describing the program algorithm with CPN, we derive an extended definition of position invariants that allows a sufficient condition for invariance to be non-linear and compute invariants, and discusses the two invariant The connection between the formulas provides a new method for constructing a cyclic invariant assertion of an algorithm.