模型检测思想和方法的演进

<正>自计算机出现以来,人们就开始寻找一种证明程序正确性的好方法。早期的程序员为验证程序的正确性,在实践中通常使用的方法是运行这一程序。然而,这种运行程序的测试方法虽然可以证明一段不正确的程序是不正确的,但无法证明一段正确的程序是正确的。因此,采用一种在数学上完备的形式验