文章目录
程序正确性
- 程序正确性
- 程序正确性证明
-
- 伪代码
- 循环不变量
- 证明
-
- 初始化
- 维护
- 终止
- 得证
程序的正确性证明是展示产品正确（满足规格说明）的一种数学技术。
许多人认为：正确性证明不能看成标准的软件工程技术。 理由是：程序员缺乏充分的数学培训；证明代价高实用性不高；证明可能是困难的。
不能如上所述一棍子打死。 就程序员的数学功底而言，取决于个人积累，而非培训。 就实用价值而言，对于严格要求正确性的情况下，正确性证明很重要。 定理证明的繁冗可以借助一部分定理证明器工具来减轻。
正确性证明的实际困难是：
- 难以认定定理证明器的准确性。
- 难以找出输入和输出规格说明，特别是找出循环不变式或出于其他逻辑状态的同等物。
- 难以保证规格说明本身准确无误。
以上困难并不能说明正确性证明对软件工程是没有意义的。反而，因为软件工程的目标是提供高质量软件，所以正确性证明有时是重要的软件工程技术。
如果根据成本-效益分析法，证明软件正确的成本低于产品
