插入排序

Posted 2020-09-12

INSERTION-SORT(A)

1 for j=2 to A.length

2   key = A[j]

3  //insertA[j] into the sorted sequence A[1...j-1]

4   i = j-1

5   while i>0 AND A[i]>key

6    A[i+1] = A[i]

7    i = i-1

8   A[i+1] = key;

把A[i...j-1]的性质形式地表示为一个循环不变式：子数组A[1..j-1]由原来在A[1..j-1]中的元素组成，但已按序排列。

循环不变式主要用来帮助我们理解算法的正确性。关于循环不变式，我们必须证明三条性质：

  初始化：循环的第一次迭代之前，它为真。

  保持：如果循环的某次迭代之前它为真，那么下次迭代之前它仍为真

  终止：在循环终止时，不变式为我们提供一个有用的性质，该性质有助于证明算法是正确的。

初始化：首先证明在第一次循环迭代之前（当j=2时），循环不变式成立。所以子数组A[1..j-1]仅由单个元素A[1]组成，实际上就是A[1]中原来的元素。而且该子数组是排序好的（当然很平凡）。这表明第一次循环迭代之前循环不变式成立。

保持：其次处理第二条性质：证明每次迭代保持循环不变式。非形式化地，for循环体的第4-7行将  A[j-1],A[j-2],A[j-3]等向右移动一个位置，直到找到A[j]的适当位置，第8行将A[j]的值插入该位置。这时子数组A[1..j]由原来在A[1..j]中的元素组成，但已按序排列。那么对for循环的下一次迭代增加j将保持循环不变式。

  第二条性质的一种更形式化的处理要求我们对第5-7行的while循环给出并证明一个循环不变式。然而这里我们不愿陷入形式主义的困境，而是依赖以上非形式化的分析来证明第二条性质对外层循环成立。

终止：最后研究在循环终止时发生了什么。导致for循环终止的条件是j>A.length=n.因为每次循环迭代j增加1，那么必有j=n+1.在循环不变式。在循环不变式的表示中将j用n+1代替，我们有：子数组A[1..n]由原来在A[1..n]中的元素组成，但已按序排列。注意到，子数组A[1..n]就是整个数组，我们推断出整个数组已排序。因此算法正确。

伪代码中的一些约定

*缩进表示块结构

*当一个for循环每次迭代增加其循环计数器时，我们使用关键词to.当一个for循环每次迭代减少其循环计数器时，我们使用关键词downto.当循环计数器以大于1的一个量改变时，该该变量在可选关键词by之后。

*符号"//"表示该行后面是个注释

*形如i=j=e的多重将表达式e的值赋给变量i和j;它应该被处理成等价于赋值j=e后面跟着i=j

*变量（如i,j和key）是局部于给定过程的。若无显示说明，我们不使用全局变量。

*数组元素通过"数组名[下标]"这样的形式来访问。

*复合数据通常被组织成对象，对象又由属性组成。我们使用许多面向对象编程语言中创建的语法来访问特定的属性：对象名后跟一个点再跟属性名。例如，数组可以看成是一个对象，它具有属性length，表示数组包含多少元素，如A.length就表示数组A中的元素数目。

  我们把表示一个数组或对象的变量看做指向表示数组或对象的数据的一个指针。对于某个对象x的所有属性f,赋值y=x导致y.f等于x.f。进一步，若现在置x.f=3，则赋值后不但x.f等于3，而且y.f也等于3.换句话说，在赋值y=x后，x和y指向相同的对象。

  我们的属性记号可以"串联".例如属性f本身是指向某种类型的具有属性g的对象的一个指针。那么记号x.f.g被隐含地加括号成(x.f).g。换句话说，如果已经赋值y=x.f，那么x.f.g与y.g相同。

  有时，一个指针根本不指向任何对象。这时我们赋给它特殊值NIL