机械验证：软件正确性与实证案例

本文探讨了软件验证中的机械化证明与程序正确性维护的关键议题。作者Wolfgang Goerigk在《理论计算机科学电子札记》58卷第2期（2001年）中提出，面对验证大型可执行机器程序的复杂性，特别是验证其非平凡正确性和高级控制结构，传统的证明方法面临挑战。作者强调了模块化编程在解决这个问题上的重要性，因为验证工作主要集中在源代码级别，而非机器代码级别。 在实践中，编译器验证被选为一个核心示例，它涉及到确保一个编译后的程序在执行时是可信的。通过这个案例，作者展示了如何应用定理证明器来检查和增强程序的正确性。另一方面，作者也承认，机械验证可能无法覆盖所有复杂情况，例如某些公式化的定理可能难以证明其正确性、实际效用有限，或者甚至存在不可证明的命题。 部分程序正确性是作者着重讨论的概念，它关注的是证明程序在特定条件下的正确行为，而非整体的无错误运行。这在实践中非常实用，因为它允许软件在满足某些假设的情况下正常工作，即使整个系统的完整正确性无法完全证明。作者引用了多篇相关文献，如[22]至[29]，这些研究强调了定期对机器可执行程序进行部分正确性验证的必要性和有效性。 文章的结论部分，作者并未放弃机械化验证的可能性，而是提倡寻找一种平衡，既要承认当前面临的局限性，也要探索如何利用现有技术和方法来提高软件验证的可靠性和效率。作者的工作得到了德国研究共同体（DFG）在Verix和VerComp项目中的支持，这些项目旨在推动正确的制造商验证技术的发展。 这篇论文不仅探讨了软件验证的实践挑战，还提出了在面对实际执行环境时，如何通过模块化方法和部分程序正确性来推进验证工作的理论与实践。