正しさは「毎周守られる約束」で言う — ループ不変式

約束は Python の assert でそのまま書けます。各周の始めに置き、最後の確認は終了時(i = n)に行います。

def insertion_sort(a):
    orig = list(a)
    n = len(a)
    for i in range(1, n + 1):
        assert a[:i] == sorted(orig[:i]), f"i={i}"   # 約束
        if i == n:
            break                                    # ③ 終了時の確認
        x = a[i]
        j = i - 1
        while j >= 0 and a[j] > x:
            a[j + 1] = a[j]
            j -= 1
        a[j + 1] = x
    return a

このままの版と、わざと1つずらした版を走らせた結果です(Python 3.14.7 / Linux aarch64、Docker の python:3.14-slim、2026-10-07)。

assert passed on 1000 random lists (len 0..30, values 0..50)
input [5, 3, 8, 1] -> fails at i=1: a=[5, 3, 8, 1] a[:i+1]=[5, 3] sorted=[3, 5]
input [1, 2, 3, 0] -> fails at i=3: a=[1, 2, 3, 0] a[:i+1]=[1, 2, 3, 0] sorted=[0, 1, 2, 3]
input [1, 2, 3, 4] -> no failure (already sorted prefix)
range start 2 -> fails at first check i=2: a[:i]=[5, 3] sorted=[3, 5]
range(2, n) start: failed 499 of 1000 random lists

正しい約束は、長さ 0〜30 の乱数列 1,000 本ですべて通りました。 確かめる範囲を a[:i+1] に広げる(まだ差し込んでいない要素まで並んでいると主張する)と、[5, 3, 8, 1] は最初の周 i=1 で落ちます。ところが [1, 2, 3, 0] は i=3 まで通り、並び済みの [1, 2, 3, 4] では一度も落ちません。

ループの開始を 1 から 2 にずらす(上のコードなら range(1, n + 1) の 1 を 2 に)と、[5, 3, 8, 1] は最初の確認 i=2 で落ちます。落ちるのは先頭2個が逆順のときだけで、長さ 2〜30 の別の 1,000 本(上の 1,000 本とは別の乱数列)では 499 本が落ちました(値が 0〜50 の一様乱数なら理論上の割合は 25/51 ≈ 0.49。499 はこの1回の乱数での値です)。壊れたコードが約半分のテストを通るということです。

第11期『半分にすると、なぜ20回で済むのか』では、二分探索を「値ではなく境目を探すもの」として見ました。その境目を、CPython は事後条件として書いています。Lib/bisect.py(3.14 ブランチ)の bisect_left の docstring です。

The return value i is such that all e in a[:i] have e < x, and all e in a[i:] have e >= x. So if x already appears in the list, a.insert(i, x) will insert just before the leftmost x already there.

HTML の公式文書は同じことを別の書き方で載せています。

all(elem < x for elem in a[lo : ip]) is true for the left slice and all(elem >= x for elem in a[ip : hi]) is true for the right slice.

同じファイルの Python 版のループです(実行時は、ファイル末尾の from _bisect import * で C 実装に置き換わります)。

while lo < hi:
  mid = (lo + hi) // 2
  if a[mid] < x:
      lo = mid + 1
  else:
      hi = mid
return lo

ここでの約束は、本教材の読みとして「a[:lo] はすべて x 未満、a[hi:] はすべて x 以上」です。最初は両側が空なので成り立ちます。どちらの枝も、確かめた側へだけ lo か hi を動かすので保たれます。終了時は lo == hi で、docstring の事後条件そのものになります。