摘要： <正> 程序正确性证明采用程序调试虽然有利于检测程序的错误,但不能保证程序是正确的;采用程序验证虽然可以证明程序正确,但困难之处在于用户必须提出一系列的中间断言作为验证条件,而寻找这组中间断言是最困难的,也是程序验证的关键。为此,本文讨论对程序的静态分析产生的解的不变式与动态测试所获得的测试值相符合的方法,以此导出程序正确性的证明。这样既避免了程序验证所须的证明一组验证条件的长而使人腻烦的工作,也避免了程序调试必须选择样品调试数据的较难克服的困难。
刘清. 一种寻找测试值断言证明程序正确的方法[J]. , 1981, 7(03): 13-21.