第9页

Correctness

To prove correctness in general, we have to reason about the program. This means three things:

We need a mathematical model of the operations of the programming language, defining what they should do. This model is called the language’s semantics.

We need to define what we would like the program to do. Usually, this is a mathematical definition of the inputs that the program needs and the output that it calculates. This is called the program’s specification.

We use mathematical techniques to reason about the program, using the semantics. We would like to demonstrate that the program satisfies the specification.

正确性

一般为了验证正确性，我们需要对程序进行推理。这意味着以下三件事：

我们需要一个定义了编程语言中的操作该做什么的数学模型。这称为语言的语义。

我们需要定义自己想要程序做什么。通常来说，这是对程序所需的输入和计算所得的输出的一个数学定义。这称为程序的规格。

我们需要使用数学技术（技巧，方式），通过语义对程序进行推理，证明程序满足了规格。