Информатика
Элементы доказательного программирования - часть 2
нач cls
ввод (а, b, с) input a, b, с
если а > b то if а > b then
тах := a max = a
инеc b > с то elseif b > с then
тах := b mах = b
инеc с > а то elseif с > a then
тах:= с mах = с
кесли end if
вывод («тах=»,тах) ? «mах=»; mах
кон end
Запуск этой программы на ЭВМ можно проверить на следующих данных:
Tecт1 Тест2 Тест3
? 1 1 2 ? 1 2 3 ? 3 2 1
max = 2 max = 3 max = 3
Все три результата правильные. Отладку программы после запуска этих примеров можно было бы считать завершенной. Однако есть контрпример:
Контрпример1
? 2 1 3
max = 2
Но этот результат - неправильный. Следовательно, алгоритм и программа содержат ошибки. Но сколько этих ошибок - одна, две, а может быть больше?
При доказательном подходе разработка алгоритмов и программ предполагает составление спецификаций и доказательство их правильности по отношению к этим спецификациям. Процесс разработки программ считается завершенным после проверки их на ЭВМ и предоставлении доказательств отсутствия ошибок.
Доказательства правильности алгоритмов и программ, равно как и любые другие доказательства, строятся на основе суждений и рассуждений.
