《算法导论》笔记——循环不变式及插入排序证明
算法导论第二章中提出了一个概念－－“循环不变式”那么，何为循环不变式
我的理解是：
“循环不变式是用于证明算法正确性的一种工具”
它应该怎么用呢
[*]首先，对于任意的一种算法，我们需要找出其循环不变式
[*]然后，需要证明循环不变式的三条性质
对于插入排序算法，它的证明是这样的：
[*]设下标j为目前正在排序的数字的索引，开始时j = 1（C++中索引从0开始，我们这里从第二个元素开始排，至于为什么，请往下读）
[*]循环不变式：“for循环每次开始时，A是有序的”
接下来我们证明三条性质：
[*]初始化 ：循环的第⼀次迭代之前，循环不变式为真
[*]保持 ：如果循环的某次迭代之前循环不变式为真，那么下次迭代之前它仍为真
[*]终止 ：终止时不变式要能做到符合结果（比如：完成排序）
证明：
1.初始化：显然，j = 1时，A就是A，只有一个数字，当然是符合循环不变式的
2.保持：若 A 有序，将 A 插入后，A 仍有序
3.终止：终止时，当 j = n 时，A 整体有序，排序完成
因此你可以看到，事实上，循环不变式就是用来规范证明算法正确性的工具
如果你对数学归纳法比较熟的话，很容易发现其实循环不变式就是数学归纳法的一个变种
如何找循环不变式？
由于算法是一步步执行的，那么如果每一步（包括初试和结束）都满足一个共同的条件，那么这个条件就是要找的循环不变式（loop invariant）
一个例子：
二分查找
不变式：若目标值存在，则必在子数组 A 中
证明要点：
初始化：l=0, r=n-1，覆盖整个数组
保持：根据中间值比较调整边界，目标值仍在新区间内
终止：l > r 时子数组为空，目标不存在 → 返回 -1
我们发现，三条性质都符合我们的要求（初始化和保持满足不变式、终止符合要求的结果），所以算法正确
循环不变式不只是理论工具——它强迫你在写循环时明确“我试图维护什么”。这种思维习惯能显著减少代码错误。
——《算法导论》核心思想
插入排序
算法原理：
插入排序与我们手动整理一副牌的过程类似（这里我们引用算法导论上的比喻）
(注意，目前为了易读，我们讨论升序排序，对于非升序，参考GitHub:《算法导论》笔记src/insertion_sort(插入排序).h中的注释
想象一下：你现在右手放着一副乱序的牌，左手开始时什么都没有
我们规定：右手的牌是无序的，左手始终有序
那么，我们现在从右手拿出一张牌，放到左手中
此时，你左手的牌仍然有序，因为此时只有一张牌，符合规定
接着，我们去拿下一张牌，这时有两种情况：
1.当前的牌面>=左手牌面
2.当前的牌面key，我们让A = A，即A = A</strong>
那么，此时A已经复制到了A，我们无论怎么操作都不会丢失A的数据，相当于腾出来了一个空位
继续执行2:此时的j = 0，A = A = 2
页:
[1]