Доказательство правильности программ | Как доказать правильность программы? (11_68_pol) (68 часов в уч. год)

Планирование уроков на учебный год (по учебнику К.Ю. Полякова, Е.А. Еремина, сокращённый курс, по 2 часа в неделю)


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



Содержание урока

Как доказать правильность программы?

Алгоритм Евклида

Инвариант цикла

Спецификация

Вопросы и задания

Задачи


Как доказать правильность программы?


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

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

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

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

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

Пример 1. Рассмотрим следующую программу для выбора максимального из трёх значений, записанных в переменных а, b и с:

если а > b то М:=а иначе М:=b все

если b > с то М:=b иначе М:=с все


Проверяя её на тестах

(а,b,с) = (1,2,3), (1,3,2), (2,1,3) и (2,3,1),

мы во всех этих случаях получаем в переменной М верный ответ 3. Однако это не означает, что программа правильная, так как существует контрпример (3,2,1): для этого набора входных данных в переменной М в результате оказывается число 2.

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

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

На практике редко доказывают правильность всей программы в целом. В то же время очень полезно доказывать правильность отдельных блоков (циклов, процедур и функций) для уменьшения количества «необъяснимых» ошибок и сокращения времени отладки.

Покажем метод доказательства правильности программы на простом примере.

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

b:=a+b	|	1
a:=b-a	|	2
b:=b-a	|	3

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

Обозначим начальные значения переменных а и b через а0 и b0. После выполнения оператора 1 в переменной b будет записано значение а0 + b0. Оператор 2 записывает в переменную а значение

b - a = a0 + b0 - a0 = b0.

В результате выполнения оператора 3 получаем новое значение переменной b, равное

b - a = a0 + b0 - b0 = a0.

Таким образом, в результате выполнения программы переменные а и b будут равны b0 и а0 соответственно, что и требовалось доказать. Поэтому приведённая программа правильная.

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

если а > b то М:=а иначе М:=b все     |1

если b > с то М:=b иначе М:=с все     |2


Анализируя строку 2, выясняем, что в ней значение переменной М всегда будет изменено, т. е. результат работы первой строки программы стирается, и

Конечно, эта величина не совпадает с определением максимального значения из а, b и с. Таким образом, программа неправильная: она выдает неверное значение, если максимальное из трёх чисел хранилось в переменной а. Контрпример мы уже приводили: (3,2,1).

Следующая страница Алгоритм Евклида



Cкачать материалы урока







Наверх