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

Метод индуктивных утверждений, о котором шла речь в предыдущей главе, можно непосредственно использовать для доказательства частичной правильности программ, написанных на каком-нибудь традиционном языке програм­мирования, например на Фортране, Алголе или ПЛ/1. Конечность таких программ можно доказывать так же, как мы это делали для блок-схем. При использовании метода индуктивных утверждений необходимо по крайней мере с одной из точек программы в каждом из замкнутых путей (циклов) связать соответствующее утверждение. Конечно, если мы используем язык программирования, то порядок выполнения (пути) неявно определяется структурой управ­ления, тогда как на блок-схемах этот порядок явно указывается стрелками. Следовательно, применяя метод индуктивных утверждений, нужно четко представлять порядок выполнения программы, чтобы быть уверенным, что не пропущен ни один из замкнутых путей в программе. Именно этот вопрос мы и рассмотрим здесь, так как сам метод утверждений мы уже описали выше, а его использование в данном случае аналогично использованию для блок-схем.

Проиллюстрируем метод на простых программах, написанных на Фортране.

Пример 3.1.

READ (5, 1) J1, J2 (Операторы READ… FORMAT производят ввод

1 FORMAT (2I10) информации по соотвнтствующему формату)

С ЗНАЧЕНИЯ, СЧИТЫВАЕМЫЕ В J1 И J2 –

С ЦЕЛЫЕ, УДОВЛЕТВОРЯЮЩИЕ УСЛОВИЯМ

С 0.LE.J1 И 1.LE.J2. (логические операции: LE – “£” ;

IQ=0 LT – “< “

IR=J1 EQ – “=”

2 IF(IR .LT.J2) GO TO 4 GE – “³”
С J1 .EQ. IQ * I2 + IR AND 0 .LE. IRGT – “>”
IQ=IQ+1 NE – “¹”
IR=IR–J2

3 GO TO 2 (C – признак комментария)

4 WRITE (6,5) IQ, IR (Операторы WRITE … FORMAT производят вывод

5 FORMAT (2I10) информации по соотвнтствующему формату)

С JL .EQ. IQ*J2 + IR AND 0.LE. IR AND
С IR .LT. J2

STOP

END

Приведенная программа на Фортране – это просто некоторый вариант программы, блок-схема которой приведена на рис. 3. Напомним, что программа вычисляет целое частное IQ и остаток IR от деления целого J1 на целое J2. Мы уже включили в качестве комментариев в программу индуктивные утверждения, необходимые для доказательства частичной правильности. Например, комментарий, помещенный сразу после оператора с меткой 2, нужно рассматривать как коммен­тарий, связанный с точкой, расположенной перед выполня­емой в этом операторе проверкой. Таким образом, предпо­лагается, что в момент прихода в точку, находящуюся непо­средственно перед проверкой в операторе с меткой 2, справедливы утверждения J1 = IQ× J2 + IR и 0 £ IR. Отметим, что в доказательствах мы используем „ = " как символ равенства, а не присваивания.

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

1. Путь от оператора READ до оператора с меткой 2. Предположим, что только что выполнился оператор READ и справедливо утверждение, записанное сразу после него. Теперь последовательно выполняются операторы до опера­тора с меткой 2. Нам нужно показать, что справедливо утверждение, записанное после этого оператора. Если мы дошли до этой точки, то имеем IQ = 0, IR = J1, 0 £ J1 и 1 £ J2. Таким образом, J1=IQ×J2 + IR=0×J2 + J1=J1 и 0£ J1= IR.

Следовательно, наше утверждение справедливо.

2. Путь от оператора с меткой 2 до оператора с меткой 3 и опять к оператору с меткой 2 (основной цикл программы). Предположим, что мы выполняем оператор 2 (мы перестаем говорить «оператор с меткой 2» и начи­наем употреблять «оператор 2». Здесь уместно отметить, что если убрать из языка программирования метки, то идентифицировать оператор станет весьма затруднительно) и справедливо записанное после него утверждение, затем выполняем цикл и возвращаемся к метке 2. Необходимо показать, что указанное утверждение снова будет справедливо. Пусть IQ и IR до выполнения цикла принимают значения IQ_N и IR_N. Тогда J1 =IQ_N • J2 + IR_N и 0 £ IR_N. При возврате к метке 2 после прохождения цикла значения IQ и IR будут IQ_N+1 = IQ_N + 1 и IR_N+1 = IR_N – J2, а значения J1 и J2 останутся без изменений. Таким образом, после возврата к метке 2 имеем

IQ_N+1 • J2 + IR_N+1 = (IQ + 1)× J2 + (IR_N – J2) =

= IQ_N ×J2 + J2 + IR_N – J2 = IQ_N • J2 + IR_N = J1.

Кроме того, известно, что если мы проходили по циклу, то проверка
IR_N .LT. J2 дала отрицательный результат, т. е. J2 £ IR. Отсюда следует, что при возврате к метке 2 имеем 0 £ IR_N – J2 = IR_N+1.

3. Путь от оператора 2 к оператору 4. Предположим, что мы выполнили оператор 2, справедливо соответствующее утверждение и переходим к оператору 4. Нужно показать, что справедливо утверждение, записанное ниже этого опе­ратора. Оператор 2 передаст управление на оператор 4 только при положительном результате проверки IR .LT. J2. При переходе от оператора 2 к оператору4 ни одно из значении переменных не изменяется, и, следовательно, при достижении метки 4 мы имеем J1 = IQ×J2 + IR, 0£IR и, кроме того, IR < J2. Таким образом, мы доказали частичную правильность.

Доказательство конечности программы на Фортране иден­тично доказательству конечности для блок-схем. Для дока­зательства конечности программы необходимо только пока­зать, что при выполнении программы мы в конце концов выйдем из единственного в программе цикла. Следовательно, надо показать, что проверка IR .LT. J2, управляющая циклом, когда-нибудь даст положительный результат. Так как значе­ние IR при каждом прохождении цикла уменьшается на вели­чину J2, a J2 остается без изменений и, кроме того, 1 £ J2, то можно заключить, что IR уменьшается каждый раз по крайней мере на 1 и когда-нибудь станет меньше J2. В этот момент условие IR < J2 станет справедливым и мы выйдем из цикла, т. е. программа закончится.

Пример 3.2.

С1 Х – ВЕЩЕСТВЕННЫЙ МАССИВ, ЕГО РАЗМЕР

С1 N .GE. 2

XSMLST = X(L)

DO 10 I = 2, N

C2 XSMLST РАВНО МИНИМАЛЬНОМУ ИЗ Х(1), ..., Х(I – 1)

С2 КРОМЕ ТОГО, 2 .LE. 1 И I .LE. N

IF (XSMLST .LE. X(I)) GO TO 10

XSMLST = X(I)

C3 XSMLST РАВНО МИНИМАЛЬНОМУ Х(1), ..., X(I – L)

C3 КРОМЕ ТОГО, 3 .LE. 1 И I .LE. N + 1

10 CONTINUE

C4 XSMLST РАВНО МИНИМАЛЬНОМУ ИЗ Х(1),..., X(N)

Предполагается, что приведенный фрагмент программы должен присвоить XSMLST значение наименьшего элемента из массива Х(1), ... , X(N). В Фортране цикл строится по следующей основной схеме:

DO метка I = M, N

С ПРИМЕЧАНИЕ 1

Тело цикла

С ПРИМЕЧАНИЕ 2

метка CONTINUE

Рис. 10.

Эта схема работает аналогично приведенной на рис. 10 блок-схеме.

Примечание 1 (комментарий), связанное с таким циклом и стоящее непосредственно за оператором DO, нужно рассма­тривать как связанное с некоторой точкой утверждение 1 на блок-схеме, а примечание 2, стоящее перед концом цикла, нужно рассматривать как утверждение 2 для некоторой точки прогр; ммы, соответствующей точке на блок-схеме.

Для доказательства частичной правильности программы нужно рассмотреть следующие пути:

1. Путь от начала фрагмента до точки 2 (точки, с которой связано утверждение 2). Если мы попадаем в эту точку, то XSMLST = Х(1) и I = 2, и очевидно, что значение XSMLST равно наименьшему из Х(1), ..., Х(I–1) = Х(2 – 1) = Х1 и
2 £ I = 2 £ N (так как N ³ 2). (Обратите внимание, что без условия N ³ 2 наше утверждение доказать нельзя, и, следова­тельно, правильная работа программы не гарантируется, если N = 1.)

2. Путь от точки 2 до точки 3 (точки, с которой связано утверждение 3). Предположим, что мы достигли точки 2, утверждение 2 справедливо, I имеет значение I_N и мы проходим по телу цикла, возвращаясь в точку 2. В теле цикла XSMLST сравнивается с Х(I_N) и, если XSMLST £ X(I_N), XSMLST остается без изменений. В противном случае значение заменяется на Х(I_N). Так как до этого известно, что значение XSMLST равно наименьшему из Х(1), ... , Х(I_N – 1), то можно легко убедиться, что теперь значение XSMLST будет равно наименьшему из Х(1), ... , Х(I_N). Однако, прежде чем мы дойдем до точки 3, значение I увеличится на 1, и, таким образом, I_N+1 = I_N + 1; следовательно, значение XSMLST снова будет равно наименьшему из Х(1), ... , Х(I_N) = Х(I_N+1–1). Кроме того, из при­мечания 2 известно, что 2 £ I_N £ N, и, следовательно, в точке 3 3 £ I_N+1 = I_N + 1 £ N + 1.

3. Путь из точки 3 к точке 2. Мы пройдем по этому пути, если только проверка I £ N даст положительный ответ. При этом условии справедливость примечания 3 приводит к справедливости примечания 2 в момент достижения этой точки.

4. Путь из точки 3 в точку 4. Мы пройдем по этому пути, если только проверка 1 £ N даст отрицательный ответ, т. е. при I > N. Но так как справедливо утверждение в примечании 3, следовательно, I = N+1, и при достижении точки 4 значение XSMLST будет равно наименьшему из Х(1), ... , Х(I – 1) = = X[(N + 1) – 1] = X(N), что и требовалось доказать, т. е. доказана частичная правильность.

Конечность этого фрагмента программы очевидна: здесь есть только один цикл, и он является фортрановским, а что конечность фортрановского цикла, следует считать свойством, присущим самому языку).

Эти два примера показывают, что метод индуктивных утверждений можно распространить непосредственно и на дока­зательства правильности программ, написанных на Фортране. Затруднение заключается лишь в том, что управление в про­граммах на Фортране не такое явное, как в блок-схемах. Это приводит к тому, что в программах легко не заметить некоторые пути или неправильно их интерпретировать (например, можно предположить, что в операторе цикла проверка выполняется перед выполнением тела цикла). Кроме того, нужно приписывание индуктивных утверждений к некоторым точкам в программе на Фортране проводить очень внимательно и все время помнить, с какой неявной точкой связано соответ­ствующее утверждение. Например, один-единственный опера­тор Фортрана, такой, как оператор DO, фактически состоит из нескольких действий: установки счетчика, увеличения счетчика и проверки. При доказательстве правильности мы должны четко осознавать, с какой из этих точек связано индуктивное утверж­дение. Использование переходов GO TO в программах на Форт­ране тоже порождает проблемы. Если в программе много пере­ходов и при их использовании не придерживались некоторой дисциплины, то программу часто трудно понимать и трудно доказывать ее правильность. Это объясняется тем, что сложно проследить за всеми возможными путями выполнения про­граммы и указать нужные для этих путей индуктивные утверж­дения. (Однако существует и иная точка зрения Если у нас есть только переходы, то программа на фортране становится полностью аналогичной блок-схеме и доказатель­ство правильности проходит так же легко, как и для блок-схем, ибо мы «видим» все точки с утверждениями. Но переходы действительно усугубляют трудности «неявных» точек, например, в операторе цикла.