主要内容
验证算法
任何算法的一个重要方面是它是 正确的：它总是根据输入产生预期范围内的输出，并最终结束。
事实证明，很难证明算法是正确的。程序员经常使用 经验分析 来查找算法中的错误，但只有 形式推理 才能证明完全正确。
经验分析
“经验”分析是基于实际实验和结果观察的分析。在算法领域，这意味着算法必须被翻译成编程语言并在计算机上执行。
让我们对算法进行实证分析，该算法是在数字列表中找到最大值。
这是表示该算法的伪代码：
maxNum ← -1
FOR num IN numbers {
if (num > maxNum) {
maxNum ← num
}
}接下来，我们将其转换为JavaScript语言，因为我们可以在Khan Academy的交互式编辑器中执行它。
var maxNum = -1;
for (var i = 0; i < numbers.length; i++) {
if (numbers[i] > maxNum) {
maxNum = numbers[i];
}
}然后我们需要将输入提供给算法并观察它的执行情况。对于我们的第一个实验，让我们给它一个4个数字的数组，
[13,4,24,7] 并查看是否输出最大值24。真棒，算法有效！我们能否宣布这是一个完全正确的算法并继续前进？我担心这不是那么容易......
这是实验 #2 的时候了。这次，让我们将数组中的所有数字设为负数，
[-13, -4, -24, -7]。这次，最大值应为 -4，即列表中最小的负数。呃哦，代码输出 -1 而不是 -4。那是因为
maxVal 的初始值是 -1，并且循环永远不会在列表中找到大于该值的值。对于负数，我们的算法肯定 不算能正常 工作。在此，我们需要修改我们的算法，对(希望)改进的算法进行实验分析。让我们尝试一个开始
maxNum至列表中的第一个数字的算法的版本：这样可行！ 或者至少，它适用于负数列表。它仍然可以在正数列表中使用吗？混合的正数和负数列表怎么样？分数怎么样？无理数呢？测试有很多可能性！
我们可以通过将算法打包到一个程序中，并使用测试库来判断程序的输出是否与我们期望的匹配，从而更容易地进行测试。 在Khan Academy，
Program.assertEqual(actual，expected) 是一个简单的测试程序，只要实际输出不等于预期值，就会显示错误。 以下是对四个不同列表的实证分析：
没有错误！新算法看起来比旧算法更正确。但真的正确吗？我们实际上并不确定。 事实上，我们可以做更多的实验并 依旧 无法确定。
经验分析只能通过发现输出意外的输入来证明实现的算法 不 正确。但是，还是无法证明算法 是 正确的。
形式推理
证明算法在所有可能输入上的正确性的唯一方法是通过形式或数学推理。
一种推理形式是“归纳证明”，这种技术也被数学家用来证明数字序列的属性。
📝 案例提示：AP CSP考试确实 不 需要了解如何通过归纳来证明算法。 我们在这里通过它来让您了解正式推理可能会是什么样子，但AP并不期望学生能够理解这种高阶的数学推理水平。
比喻可以帮助理解归纳。想象一下，我们有一百万个多米诺骨牌线，它们完美地隔开了。当我们把第一个多米诺骨牌推倒时，我们怎么知道每个多米诺骨牌都会倒下来？ 我们实际上不必检查每个单独的多米诺骨牌。我们只需要证明1）第一张多米诺骨牌会倒下来，2）翻过任何给定的多米诺骨牌都会让下一张多米诺骨牌倒下。只有这两件事证明了，就像那样，一百万多米诺骨牌将会倒下！
现在让我们将归纳法应用于算法。这是计算正整数的阶乘的算法的伪代码：
PROCEDURE calcFactorial(n) {
factorial ← 1
i ← 1
REPEAT UNTIL (i > n) {
factorial ← factorial * i
i ← i + 1
}
RETURN factorial
}数字的阶乘是该数字与所有小于它的数字的乘积，最小到数字 1。例如，
在我们开始证明这个算法成功计算
- 变量
factorial和i都从1开始。 - 由于
i(1) 不大于n(4)，我们进入循环。 - 迭代＃1：
factorial设置为1(从1 * 1)，i设置为2。 - 迭代＃2：
factorial设置为2(从1 * 2) 且i增加到3。 - 迭代＃3：
factorial设置为6(从2 * 3) 且i增加到4。 - 迭代＃4：
factorial设置为24(从6 * 4) 且i增加到5。 - 此时，
i(5) 是 大于n(4)，所以程序退出循环。 - 该程序返回值
24。
太棒了，我们验证了算法计算单个整数的正确结果。
现在让我们证明对于 所有正整数 ，算法能够计算整数的阶乘。
首先，我们需要证明算法最终会终止，因为如果算法永远运行，则算法不能被认为是正确的。在这个算法中，
i从 1 开始并增加 1 直到它变成 n + 1。因此，算法总是在 n循环重复之后停止。接下来，为了证明该算法输出阶乘，我们将更具体地证明“循环不变”，循环的属性应始终为真。在这个算法中，经过循环
n 次后，阶乘 应该等于n!并且i 应该等于n + 1。在我们对 factorial(4) 的演绎推导也是如此，现在我们将尝试证明任何正整数通常都是正确的。这需要证明 1)基本情况，以及 2) 归纳假设。
基本情况： 这是我们验证在所有的可能输入值范围内，算法是否能保存第一个数字。
对于这个算法，我们要证明它适用于所有正整数，所以基本情况是
n为1。根据循环不变量，经过循环 1 次后，factorial 应该等于1!(1) 并且 i 应该等于 1 + 1(2)。我们可以使用
calcFactorial(1) 的算法，类似于我们对数字 4 的处理方式：- 变量
factorial和i都从1开始。 - 由于
i(1) 不大于n(1)，算法进入循环。 - 迭代#1：
factorial设为1(从1 * 1)，i设为2。 - 此时，
i(2) 是 大于n(1) ，因此算法退出循环。
我们的循环不变量保存：
factorial 存储1 以及 i 存储 2。已经证明了基础案例，让我们继续往下！
归纳步骤： 这是我们展示该算法是否适用于任意数字的情形，它也适用于该数字之后的数字。
我们从归纳假设开始：假设循环不变量对于某个正整数
k 是正确的。经过循环 k 次后，factorial 应该等于 k! 并且 i 应该等于k + 1。从这个假设开始，我们将证明循环不变量也适用于
k + 1，即在 k之后的数字。经过循环 k + 1 次后，factorial 应该等于 (k + 1)! 而 i 应该等于(k + 1)+ 1。要做到这一点，让我们来看看
calcFactorial(k + 1)。由于我们的归纳假设，我们可以通过开始的 k 次重复快速到最近的一步。- 在
k次重复后，factorial存储k!和i存储k + 1。 - 迭代#
k + 1：factorial设为k! *(k + 1)并且i增加到k + 2。 - 此时，
i(其值为k + 2) 为 大于n(其值为k + 1)，因此算法退出循环。
循环不变是否成立？是的，确实成立！变量
factorial 存储 k! *(k + 1)，相当于 (k + 1)! 并且 变量 i 存储 k + 2，相当于(k + 1)+ 1。 我们可以自信地说明所有正整数
k的循环不变量都是正确的。 由于我们之前已经表明循环在
n 次重复之后停止，因此 calcFactorial(n) 总是返回n!。我们的算法是正确的，因为它终止并在终止时产生正确的答案。通过归纳证明是一种适用于循环整数算法的技术，并且可以证明算法总是产生正确的输出。其他样式的证明可以验证其他类型算法的正确性，例如通过矛盾证明或用尽证明。
这种级别的形式推理肯定存在缺陷：首先，大多数计算机程序员缺乏用证明验证的数学背景，其次，证明是在代码之外进行的，因此算法的实现可能与证明的版本不同。
最常用的使代码正确的技术是使用专门带有验证性的编程语言。亚马逊和微软等云计算公司为其关键基础设施使用可验证的语言，因为他们无法承受算法中的错误。
实际上，大多数软件都是通过实证分析验证的。这部分是由于大多数程序员缺乏证明算法正确性的理论背景。但这也是由于经验分析的简易性以及经过深思熟虑的测试套件可以证明算法几乎肯定是正确的这一事实 —— 这通常已经足够好。
🙋🏽🙋🏻♀️🙋🏿♂️您对此主题有任何疑问吗？ 我们很乐意回答-只需在下面的问题区域中提问即可！