§ 37. Доказательство правильности программ

Определения и обозначения

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

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

Тройка Хоара — запись {P} S {Q}, означающая, что при условии P выполнение программы S приводит к условию Q, если программа завершается. Здесь P — предусловие, S — команда или программа, Q — постусловие. Такая запись позволяет формулировать доказательство не расплывчато, а для конкретных исходных условий и конкретного результата.

Инвариант цикла — условие, которое сохраняется до и после каждого выполнения тела цикла и помогает доказать результат его работы. Например, при подсчёте суммы оно может связывать текущую сумму с уже обработанными числами. Инвариант нужен, чтобы обосновать каждый шаг цикла и связать его итог с постусловием.

Как это устроено

Правильность связывают с предусловием и постусловием, потому что слово «правильно» само по себе не задаёт, какие входы и какой результат имеются в виду. Сначала уточняют, что известно о данных до старта, затем формулируют требование к итоговому состоянию. Тогда доказательство отвечает на определённый вопрос: следует ли требуемый результат из исходных условий при выполнении программы.

Для присваивания нужно учесть, что меняется значение переменной, а остальные данные остаются прежними. Поэтому в постусловие подставляют выражение, присвоенное этой переменной, и проверяют, следует ли полученное условие из предусловия. Так проверка показывает не просто новое значение переменной, а то, что команда действительно обеспечивает требуемый результат.

В последовательности команд первая команда меняет состояние, с которым начинает работать следующая. Чтобы рассуждение не прерывалось между ними, формулируют промежуточное условие: оно должно следовать из результата первой команды и быть достаточным для второй. Если после последней команды выполняется постусловие, вся последовательность переводит исходное состояние в требуемое.

Ветвление выбирает одну из команд в зависимости от условия, поэтому недостаточно проверить только часто встречающийся вариант. При истинном условии проверяют первую ветвь, а при ложном — вторую; каждая должна обеспечить общее постусловие. Это доказывает правильность независимо от того, какой путь выберет программа на конкретных данных.

Для цикла заранее выбирают инвариант, который описывает полезное свойство текущего состояния. Затем доказывают, что он верен до начала цикла и сохраняется после каждого выполнения тела; иначе рассуждение не распространяется на все итерации. Наконец, условие выхода из цикла соединяют с инвариантом: вместе они должны обеспечивать постусловие, а не просто сообщать, что повторения прекратились.

Как доказывают правильность основных конструкций программы

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

Разбор задач

Задача 1. Для команды x := x + 1 докажите, что из условия x = 4 следует условие x = 5. Требуется проверить переход от заданного предусловия к постусловию именно после выполнения присваивания.

1. Запишем тройку: {x = 4} x := x + 1 {x = 5}. Предусловие сообщает исходное значение, а постусловие задаёт ожидаемый результат.
2. В постусловии вместо x подставим выражение x + 1, записанное справа от знака присваивания. Получим условие x + 1 = 5 для значения до команды.
3. Из предусловия x = 4 следует x + 1 = 5. Значит, присваивание обеспечивает постусловие. Ответ: переход доказан.

Задача 2. Программа выполняет: если x > 0, то y := x, иначе y := −x. Докажем, что после неё y = |x|. Модуль числа равен самому числу при x > 0 и противоположному числу при x ≤ 0, поэтому достаточно проверить оба случая.

1. При x > 0 выбирается первая ветвь и присваивается y = x. По определению модуля |x| = x, поэтому постусловие y = |x| выполняется.
2. При x ≤ 0 выбирается вторая ветвь и присваивается y = −x. В этом случае |x| = −x, в том числе при x = 0, поэтому постусловие также верно.
3. Других случаев для x нет, а обе ветви приводят к одному требованию. Ответ: программа устанавливает y = |x| для любого x.

Задача 3. Цикл суммирует числа от 1 до n: на каждом шаге увеличивает i на 1 и прибавляет i к s. Докажем, что после завершения s = 1 + 2 + … + n. Предположим, что перед циклом i = 0 и s = 0, а цикл выполняется, пока i < n.

1. Выберем инвариант s = 1 + 2 + … + i; при i = 0 сумма считается пустой и равной нулю. До цикла условие выполняется, потому что s = 0.
2. Пусть инвариант верен при некотором i < n. После увеличения i на 1 к s прибавляется новое значение i, то есть прежнее i + 1. Получается сумма всех чисел от 1 до нового i, значит инвариант сохраняется.
3. При выходе условие i < n ложно, то есть i ≥ n. При последовательном увеличении от 0 и остановке на границе получаем i = n; подстановка в инвариант даёт s = 1 + 2 + … + n. Ответ: требуемая сумма получена.

Типичные ошибки

• Считать программу правильной, если несколько запусков дали верный ответ. Так поступают, потому что тесты наглядны и создают ощущение проверки, но они охватывают лишь отдельные входы. Проверьте себя: доказан ли результат для любого входа, удовлетворяющего предусловию, или рассмотрены только выбранные примеры?

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

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

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

Связь с другими темами

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

Что запомнить

• Правильность программы доказывают относительно заданных предусловия и постусловия.
• Тройка Хоара записывается в виде {P} S {Q}.
• Проверка нескольких запусков не заменяет доказательство.
• Для последовательности команд важно согласовать постусловие одной команды с предусловием следующей.
• В ветвлении необходимо проверить все возможные ветви.
• Для цикла доказывают истинность и сохранение инварианта, а затем связывают его с условием выхода.