程序(Program)的正确性

怎样证明一个程序是正确的？这是一个普遍被忽略的问题。

这并不是说软件开发者们从不考虑这个问题。在一个程序的开发过程中，“正确”是所有其他工作的前提，开发者首先做的是证明程序是可以正确的，然后才来考虑性能、扩展性等等其他的问题，所以程序的正确性是所有有理智的开发者都必然会考虑的问题。

对于软件开发，“正确”通常指的是：给定一系列的测试用例和使用场景，程序能够通过这些测试，满足这些应用场景。这明显是一个不充分的定义，它把“正确性”依赖于所给的测试用例跟使用场景的完备性。假如一个程序通过了所有的测试，但在它的开发者没有考虑到的场景里面表现异常，这算不算是一种错误？如果从一开始就没有考虑到这些场景，也就是不存在“正常”又何来的异常？

"Testing shows the presence, not the absence of bugs. —— Edsger W. Dijkstra"

Edsger W. Dijkstra认为可以用形式化(formalization)的方式去证明程序的正确性。把程序看作是一种机械装置(mechanism)，给定某些输入经过一系列的操作，这个装置从状态空间(state space)内的一个状态转换到另外一个状态。大部分程序员的目标就是构造这样一种装置：它拥有合适的状态空间，包含了所有需要达到的状态；以及从输入到目标状态的坐标系统。而编程语言则是描述这种装置的一个工具。

在里面，Edsger W. Dijkstra演示了形式化证明在一些小程序中的应用。虽然这种方法在复杂的大程序中似乎很难应用，但这提供了一个新的角度来看待程序和编程。