1. 定位导航前面已经学习了算法的基本概念、运行时间分析以及插入排序的执行过程。现在要补上另一块非常重要的内容正确性证明。运行时间回答的是算法快不快循环不变式回答的是算法为什么对2. 概念术语术语定义举例循环不变式循环过程中始终保持成立的性质插入排序中左侧子数组始终有序初始化循环第一次执行前不变式成立左侧只有一个元素天然有序保持每轮循环后不变式仍然成立插入 key 后左侧仍有序终止循环结束时不变式推出正确结果整个数组已经有序正确性证明说明算法对所有合法输入都能输出正确结果不是只靠测试样例关键澄清循环不变式不是循环条件。循环不变式不是最终结果本身。循环不变式要在每轮循环前后都能成立。它的作用是把“每一步没错”连接到“最终结果正确”。3. 什么是循环不变式循环不变式可以理解成在循环执行过程中一直保持为真的关键性质。它像一条安全绳循环开始前它成立每执行一轮它仍然成立循环结束时它帮助我们推出最终结论。4. 三步证明法初始化、保持、终止4.1 初始化证明循环第一次执行之前不变式已经成立。4.2 保持假设某一轮循环开始前不变式成立证明这一轮结束后不变式仍然成立。4.3 终止证明循环结束时不变式能够推出算法的正确输出。5. 插入排序中的循环不变式插入排序可以维护这样一个不变式在每轮外层循环开始前当前下标左边的子数组已经有序并且包含的是原数组对应前缀元素的一个重排。这句话包含两个关键点第一左边部分是有序的。第二左边部分没有丢元素也没有多元素只是顺序发生了变化。6. 动态推演不变式如何贯穿排序过程下面用一个动态过程观察循环不变式如何保持。以数组[5, 2, 4, 6, 1, 3]为例插入排序每一轮都把当前key插入到左侧有序部分的正确位置。每轮结束后左侧有序部分会扩大一格。直到最后整个数组都成为有序部分。7. 用三步法证明插入排序正确7.1 初始化第一次外层循环开始前左侧只有第一个元素。一个只包含一个元素的数组天然是有序的所以循环不变式成立。7.2 保持假设某一轮开始前左侧子数组已经有序。这一轮会取出当前元素key然后从右向左扫描左侧有序部分把所有比key大的元素向右移动一格。当找到合适位置后把key放进去。因为左侧原本有序比key大的元素整体右移key被插入到正确位置所以插入后左侧扩展后的子数组仍然有序。7.3 终止当外层循环结束时已经处理完所有元素。根据循环不变式当前元素左边的部分已经有序。此时这个部分就是整个数组因此整个数组有序。所以插入排序正确。8. 如何写出一个好的循环不变式一个好的循环不变式通常要满足三点足够强循环结束后能推出最终结论能被保持每轮执行后不会被破坏容易验证初始化循环开始前可以成立。9. 代码实践用断言检查不变式defis_sorted_prefix(arr,end):foriinrange(1,end):ifarr[i-1]arr[i]:returnFalsereturnTruedefinsertion_sort_with_invariant_check(nums):arrnums[:]assertis_sorted_prefix(arr,1)forjinrange(1,len(arr)):assertis_sorted_prefix(arr,j)keyarr[j]ij-1whilei0andarr[i]key:arr[i1]arr[i]i-1arr[i1]keyassertis_sorted_prefix(arr,j1)assertis_sorted_prefix(arr,len(arr))returnarr nums[5,2,4,6,1,3]print(insertion_sort_with_invariant_check(nums))输出[1, 2, 3, 4, 5, 6]这些assert不是排序必须的一部分而是帮助我们把循环不变式显式检查出来。10. 常见误区误区一把循环条件当成循环不变式例如i n是循环条件不是证明正确性的关键性质。误区二不变式太弱比如只说“循环一直在处理数组元素”无法推出数组最终有序。误区三不变式太强如果一开始就说“整个数组已经有序”初始化通常不成立。误区四只描述过程不证明保持很多人会说“每次插入到正确位置”但没有说明为什么插入后左侧仍然有序。11. 现代延伸循环不变式不只用于排序算法它在很多工程场景中都有影子。场景类似的不变式思想数据库事务事务执行前后保持数据一致性分布式系统状态机复制要求节点状态一致缓存淘汰缓存结构始终满足淘汰策略堆结构每次插入删除后仍保持堆性质红黑树插入删除后仍保持颜色和平衡性质图算法每轮维护已确定节点集合的性质很多复杂系统的正确性本质上就是维护某种“不变性质”。12. 思考题循环不变式和循环条件有什么区别为什么插入排序中“左侧前缀有序”是一个合适的不变式初始化、保持、终止三步分别解决什么问题如果一个不变式无法推出最终结果它有什么问题尝试给“寻找最大值”算法写一个循环不变式。13. 本篇小结本篇重点讲了循环不变式。核心结论是循环不变式是循环过程中始终保持成立的关键性质正确性证明通常分为初始化、保持、终止三步插入排序中的不变式是当前元素左侧的子数组已经有序测试只能发现部分错误循环不变式可以帮助证明整体正确性。以后看到循环算法时可以多问一句这个循环到底一直维护着什么性质这句话往往就是理解算法正确性的关键。