 |
 |
 |
 |
|
 |
 |
89
алг «максимум трех чисел»
'максимум трех чисел
нач
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
Но этот результат - неправильный. Следовательно, алгоритм и программа содержат ошиб-
ки. Но сколько этих ошибок - одна, две, а может быть больше?
При доказательном подходе разработка алгоритмов и программ предполагает составление
спецификаций и доказательство их правильности по отношению к этим спецификациям. Процесс
разработки программ считается завершенным после проверки их на ЭВМ и предоставлении дока-
зательств отсутствия ошибок.
Доказательства правильности алгоритмов и программ, равно как и любые другие доказа-
тельства, строятся на основе суждений и рассуждений. В данном случае суждения и рассуждения
касаются результатов выполнения алгоритмов и программ с теми или иными данными.
Конструктивно, доказательства правильности алгоритмов и программ строятся на сужде-
ниях и утверждениях о результатах выполнения каждого из составляющих их действий и опера-
ций в соответствии с порядком их выполнения.
В качестве примера проведем анализ результатов алгоритма, состоящего из трех присваи-
ваний.
алг «у = х
5
»
Результаты
Утверждения
нач
v := х
х
v1 = х
х
v1 = x²
v := v
v
v2 = v1
v1
v2 = x
4
у := v
x
у = v2
x
у = х
5
кон
Справа от алгоритма приведены результаты выполнения присваиваний. Результатом перво-
го присваивания v := х
х будет значение v1 = х
х переменной v. Результат следующего присваива-
ния v := v
v - второе значение переменной v, равное v2 = v1
v1 . Результатом третьего присваивания
у := v
x будет значение у = v2
x .
На основе приведенных рассуждений, можно сделать три утверждения о промежуточных и
конечных результатах вычислений:
Результаты
Утверждения
{ v1 = х
х
v1 = х²
{ v2 = v1
v1
v2 = x
4
{ у = v2
x
у = х
5