Инвариант цикла - три проверки

Цикл делает неизвестное заранее число кругов, и проследить их все нельзя. Приём состоит в том, чтобы вместо всех кругов проверить один - но проверить его так, чтобы отсюда следовали остальные.

Как думаешь, что тут постоянно

summa = 0
for i in range(len(a)):
    summa = summa + a[i]

Переменная summa меняется каждый круг. И всё-таки про неё можно сказать кое-что, что верно ВСЕГДА в начале круга: summa равна сумме первых i элементов. При i = 0 сумма пуста и равна нулю; при i = 3 там a[0] + a[1] + a[2]. Это утверждение и называется инвариантом.

Инвариант цикла - утверждение, связывающее переменные, которое верно перед каждым кругом. Оно и есть замена перебору кругов: если оно верно перед первым кругом и каждый круг его сохраняет, оно верно и после последнего.

Три проверки

Инвариант доказывается ровно тремя шагами. Пропуск любого из них - типовая ошибка, поэтому они перечисляются всегда в одном порядке.

Инициализация. Инвариант верен перед первым кругом. Обычно проверяется подстановкой начальных значений, и обычно на пустом множестве: «сумма первых нуля элементов равна нулю» верно, потому что пустая сумма равна нулю.

Сохранение. Если инвариант верен перед кругом, он верен перед следующим. Это единственный содержательный шаг: здесь читается тело цикла.

Завершение. Когда цикл кончился, инвариант вместе с условием выхода даёт постусловие. Этот шаг объясняет, зачем всё делалось: без него доказано свойство, из которого ничего не следует.

Первые два шага - это индукция: утверждение проверяется для начального случая и для перехода от круга к кругу, а на все круги распространяется само. Следующая глава разбирает её отдельно.

Разбор: сортировка вставками

for j in range(1, len(a)):
    klyuch = a[j]
    i = j - 1
    while i >= 0 and a[i] > klyuch:
        a[i + 1] = a[i]
        i = i - 1
    a[i + 1] = klyuch

Инвариант внешнего цикла: перед кругом с номером j первые j элементов массива упорядочены по неубыванию и состоят из тех же значений, что были в них изначально. Вторая половина - та самая связь со входом, без которой постусловие пропускает мусор.

Инициализация. При j = 1 первый элемент один, один элемент упорядочен, и это тот же самый элемент. Верно.

Сохранение. Тело цикла берёт a[j], сдвигает вправо все элементы левой части, которые больше него, и кладёт ключ в освободившееся место. После этого левая часть длиной j+1 упорядочена: слева от ключа всё не больше него (иначе сдвиг продолжился бы), справа всё больше (их и сдвигали). Значения не потеряны: каждое либо осталось на месте, либо переехало на одну ячейку.

Завершение. Цикл кончается при j = n. Инвариант говорит: первые n элементов упорядочены и являются перестановкой исходных. Это и есть постусловие сортировки. Доказательство закончено.

Обрати внимание, чего в доказательстве нет: перебора примеров, слов «очевидно» и ссылки на то, что программа запускалась.

Разбор: инвариант двоичного поиска

levo = 0
pravo = len(a)
while levo < pravo:
    seredina = (levo + pravo) // 2
    if a[seredina] < x:
        levo = seredina + 1
    else:
        pravo = seredina

Здесь ищется первая позиция, куда можно вставить x, не нарушив порядка. Инвариант: все элементы левее levo строго меньше x, все элементы правее или равные pravo не меньше x.

Инициализация. levo = 0 - слева ничего нет; pravo = n - справа ничего нет. Оба утверждения верны пусто.

Сохранение. Если a[seredina] < x, то по упорядоченности всё до середины включительно строго меньше x, и levo = seredina + 1 инвариант сохраняет. Иначе a[seredina] ≥ x, и по упорядоченности всё от середины и правее не меньше x - pravo = seredina тоже сохраняет.

Завершение. Цикл кончился при levo = pravo. Слева от этой точки всё строго меньше x, справа всё не меньше. Значит это и есть первая позиция, где x может стоять. Постусловие получено.

Теперь сам

Сформулируй инвариант для этого цикла и скажи, что даёт шаг завершения.

schet = 0
for x in a:
    if x > 0:
        schet = schet + 1