一个不变式断言生成器

程序正确性证明是软件工程研究中一个很重要的课题。目前,程序正确性证明过程中一个最难解决的问题便是如何找出程序的不变式断言。本文在ELLOZY的基础上,对差分方程的化简公式进行讨论、简化,使得更方便、更有效地生成循环断言。我们在PDF—11机上用UCSD PASCAL语言实现了一个生成器,它能对含有数组的简单循环程序生成循环断言。