Конспект: правильность и инвариант

Понятия

Частичная корректность - если алгоритм завершился, результат удовлетворяет постусловию. Про остановку не говорит ничего.

Завершаемость - алгоритм завершается на любом входе, допущенном предусловием.

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

Инвариант цикла - утверждение о переменных, верное перед каждым кругом. Внутри тела оно может временно нарушаться.

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

Контрпример - один вход, на котором постусловие нарушено. Доказывает неверность окончательно.

Три шага доказательства инвариантом

Что унести

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

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

Инвариант пишется до кода. Тогда границы цикла и знаки сравнения выводятся, а не подбираются: +1 ставится там, где без него утверждение станет ложным.

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

Инвариант двоичного поиска: левее levo всё строго меньше x, правее или равное pravo - не меньше x. Отсюда сразу видно, где ставить единицу.

Мера не обязана быть счётчиком. Длина отрезка, остаток от деления, размер оставшихся данных - всё это меры, и ни одна из них не говорит числа кругов заранее.

Общего способа проверить остановку машиной нет: неразрешимость проблемы останова доказана. Меру называет автор, а не инструмент.

Ловушки джокера

Доказал инвариант и решил, что закончил. Без меры остаётся программа, которая на одном входе из тысячи висит и никогда не выдаёт неверного ответа.

Сформулировал инвариант только про результат. «Левая часть упорядочена» без «и это перестановка исходной» пропускает цикл, заполняющий её нулями.

Пропустил шаг завершения. Доказано верное утверждение, из которого постусловие не следует. Такое доказательство ничего не стоит.

Написал levo = s вместо levo = s + 1. Мера перестаёт убывать при отрезке длины один, и цикл идёт вечно. Инвариант при этом цел.

Проверил, что цикл работает, вместо того чтобы назвать меру. Гипотеза Коллатца проверена до 2⁶⁸ и не доказана до сих пор.

Проверь себя

Почему программа, зацикливающаяся на любом входе, частично корректна?

Какие два утверждения входят в инвариант сортировки вставками и что случится, если оставить только первое?

Какая мера у цикла while b != 0: a, b = b, a % b и что из неё следует, кроме конечности?

Где в двоичном поиске стоит +1, где не стоит и почему асимметрия не случайна?