无错误编程
 |
 | 注意：请带着批判的眼光看待下面的文章。编写无错误的代码是不可能的。最好的开发者专注于编写可靠且可维护的代码，但任何声称一段代码是无错误的人都没有做好功课。 |
研究表明，最优秀程序员和最差程序员的生产力之间存在 20 倍的差距。也就是说，顶级程序员的工作效率是差劲程序员的 20 倍，大约是平均程序员的 5 到 10 倍。这意味着一个非常优秀的开发者可以在一天内完成其他人可能需要一个月才能完成的工作。提高生产力有几种方法，但最重要的因素是准确性。
准确性与开发速度密切相关。最优秀的开发者从一开始就通过编写无错误的代码来脱颖而出。如果您能够编写不包含任何错误的代码，您就不必浪费时间寻找错误。曾经想过为什么隔壁桌那个悠闲工作的人做事比你快得多？那是因为他第一次就做对了。当然，完全防止错误是不可能的，但是
快速工作意味着准确工作，而不是努力工作。
那么如何编写无错误的代码？您可能会认为大多数错误是由粗心大意造成的，但实际上，大多数错误是由程序员没有完全理解自己的代码造成的。如果您在 Java 中遇到 NullPointerException，这通常不是因为您忘记考虑空引用，而是因为您没有真正理解空引用的变量的作用。
无错误编程的关键是牢固理解您编写的代码。
要编写无错误的代码，您首先必须学习如何证明一段代码有效。许多开发者在大学里学习这些技术，但他们从来没有真正学会在实际编码中应用这些技术。其他开发者（尤其是那些没有学位的人）一开始就没有学习形式化方法，所以这是一个很好的起点。乍一看它可能过于理论化，但这是无错误编程的关键。
让我们从一个非常简单的程序开始。这里目标是当程序终止时，类型为int的变量x包含值 10。我们将使用 C++ 在整本书中进行演示。
int x; x = 10;
这段代码显然是无错误的。为了证明这一点，让我们在代码的每一行前后添加用大括号括起来的条件。条件是逻辑语句，在执行时间条件所在的点上是正确的无论执行如何到达那里。
{true}
int x;
{true}
x = 10;
{x == 10}
前两个条件为真，因为我们在这两个点上没有任何信息（注意，C++ 不预先初始化变量）。我们唯一知道的是那里是true本身。但是，在执行完x = 10这一行之后，我们知道x的值是10，因为这是赋值的定义。我们可以用更通用的术语来表达这一点
{true} x = a {x == a}
这意味着，无论之前是什么，在将a赋值给x之后，x==a将为真，即x的值将是a。我们将把它视为常量赋值的公理。
下面的程序也为x赋值10，但它采用了不同的方式。
int x, y; y = 10; x = y;
为了证明它是正确的，用条件再次对其进行注释
{true}
int x, y;
{true}
y = 10;
{y == 10}
x = y;
{x == 10}
在对y赋值之后，我们可以说它的值是10。好吧，如果y是10，我们将其赋值给x，x也会是10。这将导致赋值的完整公理
{y == a} x = y {x == a}
类似的规则适用于赋值右侧有表达式的情况。另一个重要的公理是，赋值不会改变任何未赋值的变量。
{y == a} x = b {y == a}
这仍然非常微不足道，只需要围绕它构建其他部分。
您可能已经意识到，关于每个赋值，有两个条件需要考虑：一个是它之前成立的条件，另一个是它之后成立的条件。前者称为前置条件，后者称为后置条件。我们将通过将它们链接来证明程序的正确性：一个语句的后置条件是下一个语句的前置条件。
if {P} S1 {R} and {R} S2 {Q} then {P} S1; S2 {Q}
这里S1; S2表示两个语句一个接一个地执行，即按顺序执行。还有另外两种类型的控制结构：条件语句和循环语句。我们将在后面学习如何推理它们。
我们开始正式的正确性证明所需要的最后一个公理是
if P => R and {R} S {T} and T => Q then {P} S {Q}
A => B表示A在逻辑意义上蕴含B。
如果这一切对你来说都是天书，不要惊慌。我们将涵盖足够的示例，让这些东西开始变得有意义。
现在让我们进行第一个正式的正确性证明。证明以下程序将10赋值给x。
int x, y, z; z = 1; y = 2 * z; x = y * 5;
对其进行注释
{true}
int x, y, z;
{true}
z = 1;
{z == 1}
y = 2 * z;
{y == 2}
x = y * 5;
{x == 10}
我们有了注释，但我们必须证明它们确实在它们被写到的点上成立。
{true} int x, y, z {true}
这很简单，因为变量定义从正确性的角度来看没有任何作用。现在我们必须证明
{true} z = 1 {z == 1}
这是因为赋值的公理。由于它是一个公理，我们不需要进一步证明它。我们现在可以使用它作为下一个语句的前置条件
{z == 1} y = 2 * z {y == 2}
再进行一次
{y == 2} x = y * 5 {x == 10}
为什么这证明了原始语句？如果我们像这样命名语句和条件
{Q1: true}
S1: int x, y, z;
{Q2: true}
S2: z = 1;
{Q3: z == 1}
S3: y = 2 * z;
{Q4: y == 2}
S4: x = y * 5;
{Q5: x == 10}
并使用顺序公理三次，我们得到
{Q1} S1 {Q2} and {Q2} S2 {Q3} => {Q1} S1; S2 {Q3}
{Q1} S1; S2 {Q3} and {Q3} S3 {Q4} => {Q1} S1; S2; S3 {Q4}
{Q1} S1; S2; S3 {Q4} and {Q4} S5 {Q5} => {Q1} S1; S2; S3; S4 {Q5}
我们本质上证明了整个程序从{true}（无论是什么）到{x == 10}（x的值为10）。
这就是我们必须证明的，才能 100% 绝对确定代码是无错误的。请注意，现在毫无疑问，这段代码是正确的（当然，除非我们在证明中犯了错误）。这之所以成为可能，是因为我们对代码在每个可能的执行点上所发生的事情有非常清楚的理解。用条件对代码进行注释使我们的期望变得明确，并且不得不以正式的方式来证明它们让我们思考了为什么这些期望是正确的。
在现实生活中，没有人有时间进行正式的正确性证明，但了解如何进行这些证明对创建无错误的代码有很大帮助。关键是要明确期望。这可以防止您忘记null引用，以及其他一些事情。
让我们继续讨论条件语句。
int x, y;
if (x % 2 != 0)
{
y = x + 1;
}
else
{
y = x;
}
我们想在这里证明y在最后是偶数。条件语句的公理如下
given {P && R} S1 {Q} and {P && !R} S2 {Q} => {P} if R S1; else S2 {Q}
要证明条件语句是正确的，您必须证明两件事。首先，您必须证明当条件为真时，“then”子句会给出正确的结果。其次，您必须证明当条件为假时，“else”子句会给出正确的结果。对前面的示例进行注释
{true}
int x, y;
{true}
if (x % 2 != 0)
{
y = x + 1;
}
else
{
y = x;
}
{y % 2 == 0}
As for the variable definitions:
{true} int x, y {true}
检查。我们没有明确地为x赋值，但我们将证明使用其值的程序的正确性。C++ 不预先初始化局部变量。变量的值是某些内存垃圾。我们这里有一个条件语句，所以我们必须分别检查then和else子句。
{Q1: true && x % 2 != 0} y = x + 1 {R1: true && y == x + 1 && x % 2 != 0}
显然
true && y == x + 1 && x % 2 != 0 => (y - 1) % 2 != 0 => y % 2 == 0
现在，如果您使用松弛公理
{Q1} y = x + 1 {R1} and R1 => y % 2 == 0
----------------------------------------
{Q1} y = x + 1 {y % 2 == 0}
现在让我们来处理else子句
{Q2: true && !(x % 2 != 0)} y = x {R1: true && y == x && !(x % 2 != 0)}
显然
true && y == x && !(x % 2 != 0) => y == x && x % 2 == 0 => y % 2 == 0
同样，使用松弛公理
{Q2} y = x {R2} and R2 => y % 2 == 0
------------------------------------
{Q2} y = x {y % 2 == 0}
现在将结果与条件语句的公理结合起来
{true && R} y = x + 1 {y % 2 == 0} and {true && !R} y = x {y % 2 == 0}
----------------------------------------------------------------------
{true} if R y = x + 1; else y = x {y % 2 == 0}
我知道您不相信它在现实生活中真的有用，但请继续阅读。我们最终将放弃数学，只使用证明的核心概念来生成无错误的代码。
让我们编写第一个包含一些实际值的程序。假设我们有一个int数组，我们想将它的元素之和放入一个名为sum的变量中。我们将在本示例中学习如何推理循环，这将是您第一次看到它如何帮助您立即编写正确的代码。我们将从一个预先制作的程序开始，但稍后我们将研究如何将正确性证明中使用的技术转换为代码设计。
int[] array;
int length;
// Fill the array.
{Q: array has been created and has at least length elements and length >= 0}
int i, sum;
i = 0;
sum = 0;
while (i != length)
{
sum = sum + array[i];
i = i + 1;
}
{R: sum = array[0] + array[1] + ... + array[length-1]}
前置条件Q的声明是为了确保我们不会尝试读取未分配的内存。在本示例中，我们不关心数组是如何分配的或如何填充数字的。
循环是三种控制结构中最复杂的，也是最容易出错的。困难在于循环是伪装的条件语句序列，您甚至不知道它是多少个条件语句，因为它取决于运行时评估的条件。如果您尝试通过可视化循环的执行方式来推理循环，那么您将遇到麻烦，尤其是当您拥有比上一个循环更复杂的循环时。可视化是了解如何编码某件事的一个重要步骤，但是如果您不想在截止日期前花时间调试没有可视化的边缘情况，那么您最好静态地推理您的代码。这并不一定意味着数学上。我们最终将完全放弃数学。
关键是将循环的动态特性转换为静态条件。如果我们能够证明一个在每次评估条件之前都成立的条件，那么我们就可以推理循环，而不依赖于可视化。这个条件称为循环的不变式。
{Q: array has been created and has at least length elements and length >= 0}
int i, sum;
{Q}
i = 0;
{Q && i == 0}
sum = 0;
{Q && i == 0 && sum == 0}
while (i != length)
{
sum = sum + array[i];
i = i + 1;
}
{R: sum = array[0] + array[1] + ... + array[length-1]}
在本示例中，我们只关心循环，因为其余部分很简单。不变式是sum包含从索引1到索引i-1的元素之和每次在评估条件之前，包括第一次执行到达循环时。
{I: sum == array[0] + ... + array[i-1]}
当执行到达循环时
{Q && i == 0 && sum == 0}
成立。它是否蕴含I？当然
Q && i == 0 && sum == 0 => sum = 'sum of elements from 0 to -1'
这是真的，因为索引0和索引-1之间没有元素，而0个数字的总和为0。也就是说，空数组所有元素的总和为0。如果数组不为空，则循环体将执行，并且条件将再次评估。此时I为真（我们不考虑具有副作用的循环条件，稍后将详细介绍）。循环条件也为真，因为否则我们不会进入循环体。我们要证明的是
{I && i != length}
sum = sum + array[i];
i = i + 1;
{I}
也就是说，不变量在迭代之间保持不变。语句之间使用什么条件？sum已更新，但i未更新。试试
{Q1: sum == array[0] + ... + array[i-1] && i != length}
sum = sum + array[i];
{Q2: sum == array[0] + ... + array[i-1] + array[i] && i != length}
i = i + 1;
{I}
我们能证明
{Q1} sum = sum + array[i] {Q2}
吗？我们这里有一个小问题，因为我们无法证明array[i]是一个有效的表达式。i必须小于length且至少为0才能有效。此外，我们需要将数组分配为至少具有length个元素的数组（为了节省空间，我们将此条件表示为T）。因此，我们必须修改我们的不变量以包含此信息。
{I: T && 0 <= i && i <= length && sum == array[0] + ... + array[i-1]}
请注意理解我们编写的代码中的这一重要步骤。我们没有将所有期望明确化。这就是错误潜入的方式。使用这个新的不变量，我们必须从头开始。当执行命中循环时，它是真的吗？
T && length >= 0 && i == 0 && sum == 0 => T && 0 <= i && i <= length && sum = 'sum of elements from 0 to -1'
这是真的。例如，我们知道i <= length，因为i == 0且length >= 0。它在迭代之间保持不变吗？
{Q1: T && 0 <= i && i <= length && sum == array[0] + ... + array[i-1] && i != length}
sum = sum + array[i];
i = i + 1;
{I}
更新sum后找到正确的条件
{Q1: T && 0 <= i && i <= length && sum == array[0] + ... + array[i-1] && i != length}
sum = sum + array[i];
{Q2: T && 0 <= i && i <= length && sum == array[0] + ... + array[i-1] + array[i] && i != length}
i = i + 1;
{I}
我们知道array[i]是有效的，因为i上的约束包含在条件中。关于
{Q2} i = i + 1 {I}
?
{Q2: T && 0 <= i && i <= length && sum == array[0] + ... + array[i-1] + array[i] && i != length}
i = i + 1;
{Q3: T && 0 <= i-1 && i-1 <= length && sum == array[0] + ... + array[i-1] && i-1 != length}
我们将i更改为i-1，因为它是在执行语句之前i的原始值。
Q3 => I
因为
T && 0 <= i-1 && i-1 <= length && sum == array[0] + ... + array[i-1] && i-1 != length => T && 0 <= i && i <= length && sum == array[0] + ... + array[i-1]
例如，0 <= i-1意味着1 <= i，进而意味着0 <= i。i-1 <= length和i-1 != length一起意味着i-1 < length，进而意味着i <= length。
当循环终止时，其条件为假。此外，不变量为真。这是因为它每次在评估条件之前都为真。如果我们能证明
I && !(i != length) => R
我们就证明了当循环终止时R为真。这是微不足道的
T && 0 <= i && i <= length && sum == array[0] + ... + array[i-1] && i == length => sum = array[0] + array[1] + ... + array[length-1]
我们已经证明，如果程序终止，它将给出正确的结果。但是请注意，我们尚未证明它实际上会终止。这称为部分正确性。完全正确性意味着还要证明程序会终止。我们将在后面详细讨论。
确保您理解以上内容。我只给出了几个例子，因为这不是关于形式正确性证明的书。如果您觉得需要更深入地了解它，请查阅一些关于 Hoare 方法的书籍。如果您不理解它，本书的其余部分将毫无意义。
那么这如何帮助您更快地工作呢？您没有时间一直进行代码的形式证明，但了解如何进行形式证明将有助于您，即使您没有使用它。对先决条件、后置条件和不变量的充分理解将帮助您编写更好的代码。现在，我们将介绍大量示例来说明这一点。