伪代码：

image.png

排序示意图：

image.png

我们把A[1..j-1]的这些性质形式地表示为一个循环不变式，循环不变式主要用来帮助我们理解算法的正确性。关于循环不变式，我们必须证明三条性质：

• 初始化：循环的第一次迭代之前，它为真。
• 保持：如果循环的某次迭代之前它为真，那么下次迭代之前它仍为真。
• 终止：在循环终止时，不变式为我们提供一个有用的性质，该性质有助于证明算法是正确的。

JAVA代码实现：

Integer[] arr = {15, 22, 41, 16, 11, 31};
for (int i = 1; i < arr.length; i++) {
      System.out.println(arr[i]);
      int key = arr[i];
      int j = i - 1;
      while (j >= 0 && arr[j] > key) {
          arr[j + 1] = arr[j];
          j = j - 1;
      }

      arr[j + 1] = key;
}

输出结果：

image.png