软件程序正确性证明，测试可以暴露程序中的错误，因此是保证软件可靠性的重要手段；但是，测试只能证明程序中有错误，并不能证明程序中没有错误。因此，对于保证软件可靠性来说，测试是一种不完善的技术，人们自然希望研究出完善的正确性证明技术。一旦研究出实用的正确性证明程序（即能自动证明其他程序的正确性的程序），软件可靠性将更有保证，测试工作量将大大减少。但是，即使有了正确性证明程序，软件测试也仍然是需要的，因为程序正确性只证明程序功能是正确的，并不能证明程序的动态特性是符合要求的。此外，正确性证明过程本身也可能发生错误。

  正确性证明的基本思想是证明程序能完成预定的功能。因此，应该提供对程序功能的严格数学说明，然后根据程序代码证明程序确实能实现它的功能说明。在20世纪60年代初期，人们已经开始研究程序正确性证明的技术，提出了许多不同技术方法。虽然这些技术方法本身很复杂，但是它们的基本原理却是相当简单的。

  如果在程序的若干点上，设计者可以提出关于程序变量及它们的关系的断言，那么在每一点上的断言都应该永远是真的。假设在程序的P1、P 2、…、Pn" 等点上的断言分别是a（1）、

a（2）、…、a（n），其中a（1）必须是关于程序输入的断言，a（n）必须是关于程序输出的断言。

  为了证明在点Pi 和Pi+1之间的程序语句是正确的，必须证明执行这些语句之后将使断言a（i）变成（i+1）。如果对程序内所有相邻点都能完成上述证明过程，则证明了输入断言加上程序可以导出输出断言。如果输入断言和输出断言是正确的，而且程序确实是可以终止的（不包 含死循环），则上述过程就证明了程序的正确性。

  人工证明程序正确性，对于评价小程序可能有些价值，但是在证明大型软件的正确性时，不仅工作量太大，更主要的是在证明的过程中很容易包含错误，因此是不实用的。为了实用的目的，必须研究能证明程序正确性的自动系统，人工智能研究正在进行这方面的工作并已取得重要进展。