关于程序验证方法的讨论

On Methods of Program Verification

一、引言 自从1967年Floyd发表其论文“给程序赋予意义以来,程序自动验证工具的研究持续了数十年。Floyd在文[4]中提出了用“断言式方法”证明程序的正确性。

The researching in the program correctness verification has been taken decades,but so far as we know no substantial progress has been made. In this paper,we attempt to discuss the prob-lem,including a discussion on the weakness in traditional methods and existance of a new method.