Верификация (доказательство правильности) программ с помощью математической логики

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

Пусть, а — программа, Р — предусловие, относящееся к входным данным, которое должно быть истинно перед выполнением программы a, Q — постусловие, которое должно быть истинно после выполнения программы а.

Программа, а — частично правильная (P[a]Q) относительно предусловия Р и постусловия Q, если всякий раз, когда перед выполнением, а предусловие Р истинно для входных значений переменных и оператор, а завершает работу, постусловие Q также будет истинным для выходных значений переменных.

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

Пример 5.1.

Докажем по индукции корректность программы на C++для вычисления квадрата натурального числа. Пусть Q (n) = (п — натуральное число). Имеем следующую программу.

unsigned char s, к, п;

main () {s = О/.

for {к = 1; к < = л; к++)

// A (s, к) = к²

s = s + 2 к +1;

// В (s, к) = (s = (к + I)²).

}.

Пусть P (s, п) = (s = п²) — предикат после п-го прохода цикла, a s_k — значение переменной после k-ro прохода цикла. Шаги индукции:

• 0)$, = I²;
• (2) если s_k = k²_y то s*₊₁ = (k +1)² = k²+ 2k + 1.

Очевидно, что после первого прохода цикла = 1 и пункт (1) выполнен. Предположим, что после /г-й петли цикла s^= k². Тогда после следующего прохода.

Таким образом, пункт (2) тоже имеет место.

Р (1) = 1 истинно, Р (2) = 1 + 2 + 1 = 2², …, связка P (k) —> P (k +1) справедлива при любом k > 1. Согласно принципу математической индукции Р (п) истинно для всех натуральных п.

Цикл for ограничен определенным числом итераций (проходов). В том случае, когда число нетель цикла заранее не определено, как в цикле while … do, при доказательстве индукцией следует предположить, что число проходов все же ограничено, показать правильность выходных данных и проверить, что число петель такого цикла конечно.

Для доказательства частичной правильности операторных программ обычно используются различные модификации метода Флойда. На схеме программы выбираются контрольные точки, так чтобы любой циклический путь проходил по крайней мере через одну точку. С каждой контрольной точкой ассоциируется специальное условие (инвариант цикла), которое истинно при каждом переходе через эту точку.

С входом и выходом схемы также ассоциируются преди постусловия. Затем каждому пути программы между двумя соседними контрольными точками сопоставляется так называемое условие правильности. Выполнимость всех условий правильности гарантирует частичную правильность программы.

Одна из модификаций метода Флойда заключается в построении аксиоматической системы (логики Хоара^[1]), состоящей из схем аксиом и правил вывода, в которой в качестве теорем выводимы утверждения о частичной правильности программ, на алгоритмическом языке программирования.

Пример 5.2.

Требуется составить программу, которая для любых натуральных х и у определяет, делится ли х на у, или «х/у». Тогда определение делимости можно записать следующим образом: существует ли такое п, что пу = х?

Заменим условиех = у + у + … + у (п слагаемых) на равносильное ему: 0 — ху — -у-… — г/ (п вычитаемых). Проверка этого условия уже под силу компьютеру: нужно организовать цикл, который на каждом шаге вычитает сначала из х число г/, затем из результата снова у, и так до тех пор, пока не получится число 0 (ответ истинный) или отрицательное число (ответ ложный).

Итак, условие, налагаемое на входные данные: х е N, у е N (N — целые числа); условие, которое необходимо проверить: 2 = 0. Докажем правильность структурной схемы программы методом от противного.

Суть этого метода состоит в следующем. Допустим, что требуется доказать утверждение, А Мы принимаем гипотезу о том, что А ложно, т.с. истинно —А. Если из —А удается вывести противоречие В v ->В, то заключаем, что —А на самом деле ложно (поскольку влечет противоречие). Значит, истинно А.

Требуется доказать, что выдача нашей программой результата 2 = 0 будет происходить в том и только в том случае, когда х делится на у. Это значит, что доказываемое утверждение А имеет вид «2 = 0 —> х/у».

Допустим, что это утверждение неверно. Это означает, что ложно одно из утверждений «2 = 0 —> х/у» ИЛИ «х/у —> 2 = 0».

Предположим, что ложна первая импликация «2 = 0 —>х/у», г. е. 2 = 0 истинно, но х на у не делится. В соответствии со структурной схемой 2 = 0 либо когда х = 0, либо когда в процессе вычитания х — у — у — … — у на некотором шаге получится 0. В первом случае х делится на у, и получаем противоречие с допущением. То же происходит и во втором случае. Если х — у — у — … — у = 0, то «г — пу = 0, т. е. х = пу для некоторого п, что и означает делимость х на у.

Допустим, что ложна вторая импликация, т. е. что х делится на г/, но z Ф 0. Неравенство z Ф 0 может иметь место в одном из следующих трех случаев:

• а) при невыполнении условия х > у, т. е. при х <�у
• б) после завершения цикла;
• в) в ходе выполнения цикла.

Поскольку присваивание z := х при х Ф 0 приводит к вхождению в цикл (так как из х Ф 0 следует х > 0, z > 0) и никаких других возможностей для z Ф 0, кроме указанных трех, на структурной схеме не существует, рассмотрим последовательно эти три возможности:

• а) если х < г/, то по структурной схеме z := -1, т. е. z Ф 0, а значит, х не делится на у и противоречие с допущением;
• б) если цикл завершен и z Ф 0, то z < 0. Это означает, что х — ку < 0, т. е. х <�ку и -п (3п е N)(# = пу). Следовательно, х не делится на г/, что также противоречит допущению;
• в) z Ф 0 в ходе выполнения цикла. Но в этом случае не требуется, чтобы был дан ответ на вопрос о делимости х на у. Предполагается возможность его получения после выполнения программы, а не в ходе ее выполнения. Но только что было доказано, что если цикл завершится с z Ф 0, то х на у не делится. Здесь обнаруживаем, что цикл может и не завершиться, если z будет оставаться положительным. Эго будет происходить в том случае, когда y = 0uz-0 = z = x>0. Но так и должно быть: ведь в этом случае мы будем пытаться установить, делится ли положительное число х на нуль, а такая операция запрещена.

Таким образом, устанавливается, что если программа завершится, то будет решена поставленная задача, что доказывает частичную правильность программы. Чтобы программа была тотально правильной, нужно предусмотреть ее завершение и в выявленном исключительном случае. Например, перед проверкой условиях>у проверяется утверждение «х> 0 & у = 0». Если оно истинно, то переходим к присваиванию z := -1, если же оно ложно, то к проверке х > у.

• [1] Гуц А. К. Математическая логика и теория алгоритмов. М.: Либроком, 2009.