43
Проверка правильности алгоритмов
Кандидат технических наук
В. А. КАЙМИН
Составление программы — это искусство, наука или ремесло? Можно ли составлять программы и гарантировать, что в них нет ошибок? Эти два вопросы — предмет жарких научных дисциплины, столковения меней и сервисных исследований. Попробуем разобраться.
Можно выделить три подхода к составлению программы для вычислительных машин.
Первый подход — называем его традиционным — состоит в написании программы на некотором языке программирования (бейсик, фортран, ПЛ/1, кобол и т.п.) сразу по содержательным формulierовкам задач:
Языки программирования, как правило, имеют английскую лексику, и программы на этих языках трудно читать, понимать и изучать лодям, для которых английский язык не является родным. При составлении программы при традиционной практике почти всегда в них вносится большое число ошибок, и составитель программы как можно скорее стремится выйти на ЭВМ и начать отладку программы.
Количество ошибок в программе заранее никогда не известно, а потому никакому не известно, когда закончится отладка программы. Более того, когда авторы программы заявляют, что их программы полностью отладены, в этих программах обычно еще имеются ошибки.
Второй подход к составлению программы, который принято называть структурным программированем, состоит в тщательном продумывании логики решения задачи и создании структурированных алгоритмов. Эти алгоритмы мы советуем записать на школьном алгоритмическом языке из вашего учебника и только после этого переводить запись программы на один из языков программирования. Схему составления программы можно
44
изображать так:
При таком подходе легко разделить синтаксические и алгоритмические ошибки. Синтаксические ошибки (нарушения правил языка программирования) могут появиться только при неправильном кодировании программы по алгоритмам. Алгоритмические ошибки (нарушения в логике решения задач) возникают при составлении алгоритмов; их поиск и исправление может проводиться по описаниям алгоритмов до написания и испытания программы на ЭВМ.
Третий подход, который мы называем систематическим конструктивным программ, является развитемового. Схематически его можно изображать следующей диаграммой:
Более подробно об этом подходе расскажано в «Кванте» (1986, № 10, с. 47 и № 11, с. 40).
Проверка программы на ЭВМ включает тщательно спланированные испытания на соответствие работы машин сценарию программы. Проверка состоит в проверении всех основных частных случаев постановок задач, проверке граничных условий, проверке реакций программы на недопустимые данные и недопустимые действия со стороны человека. На этой стороне — связанной со сценарием диалоговых программ (см. «Кванте», 1986, № 11, с. 40) — мы здесь подробнее остановывать не будем.
Выявление ошибок и обоснование правильности программы при таком подходе проводится путем логических рассужждения, целую которых является доказательства — будет или не будет программы давать требуемые результаты и сообщения? Полная гарантия отсутствия ошибок возможна только при наличии математических постановок решаемых задач и детальном описании сценария работы с ЭВМ.
В этой ситуации программы мы называем правильной, если при любых допустимых исходных данных она формирует результаты, строго соответствующие сценарию при любых действиях пользователя. Программа содержит ошибки, если можно указать такие данные, при которых машина дает результаты, противоречащие сценарию постановок решаемых задач, либо ее работа не будет соответствовать описанию сценария программы.
Мы рассмотрим здесь несколько примеров обоснования правильности отдельных фрагментов программы, написанных на школьном алгоритмическом языке (часть заголовка программы для краткости опускаем).
Пример 1 (задча на вычисление).
алг «вычисление x⁵»
нач v := x · x
v := v · v
y := v · x
результаты
v₁ = x · x,
v₂ = v₁ · v₁,
y = v₂ · x.
Обратите внимание, что переменной v в процессе работы алгоритма происходит неописание несколько значений, поэтому в записи результатов мы сначала букву v числовыми индексами. На основании этой программы мы делаем следующее
Утверждение. y = x⁵.
Доказательство. Из описания результатов выполнения операций имеем
y = v₂ · x = (v₁ · v₁) · x =
= ((x · x) · (x · x)) · x = x⁵.
Пример 2 (алгоритм с учетом ветвления).
алг «вычисление |x|»
нач если x > 0
то y := x
иначе y := -x
результаты
x при x > 0,
-x при x ≤ 0.
Утверждение. Эта программа всегда дает y = |x|.
Доказательство проводится разбором случая. При x > 0 выполняется первая альтернатива. В результате присавания величины станет равной y = x, что соответствует опре-