Petri网在程序正确性证明中的应用研究

Ｆｌｏｙｄ的循环不变式断言法是部分正确性证明的常用方法之一，但循环不变式断言的构造是比较困难的，而染色网（ＣＰＮ）的位置不变量是可求出的．本文通过用ＣＰＮ描述程序算法，引出了一种拓广的位置不变式的定义，此定义允许不变式是非线性的，以及计算不变式的一个充分条件，并且讨论了上述两种不变式之间的联系，为构造一算法的循环不变式断言提供了一种新的方法．

On Loop Invariant in Nonlinear Form for Proving Correctness of Software

In software engineering, the loop invariant assertion of Floyd [1] is still widely used fo rproving correctness of programming. But the construction of such assertion is very difficult'We now present our research results on how to reduce greatly this difficulty.The said difficulty can be much reduced through our modification of Jensen's idea [4][5]= extension of Jensen's invariant for colored Petri Net (CPN) from only in linear form toan invariant for CPN in noallnear form. For our extension to be applicable, it is necessarythat the following condition must be satisfied: the weight functions defined by user are linearfor all "nonclear" places.Finally we present an example in convenient graphical form (Figs. 1 and 2). Fig. 1 givesa program for calculating the square of positive integer m, Fig. 2 gives its correspondingCPN. These figures show that our extension of Floyd's idea is feasible.