Теория вычислительных процессов Лекция ДОКАЗАТЕЛЬСТВО ПРАВИЛЬНОСТИ ПРОГРАММ, НАПИСАННЫХ НА ОБЫЧНЫХ ЯЗЫКАХ ПРОГРАММИРОВАНИЯ Преподаватель: Веретельникова. - презентация

1 Теория вычислительных процессов Лекция ДОКАЗАТЕЛЬСТВО ПРАВИЛЬНОСТИ ПРОГРАММ, НАПИСАННЫХ НА ОБЫЧНЫХ ЯЗЫКАХ ПРОГРАММИРОВАНИЯ Преподаватель: Веретельникова Евгения Леонидовна 1

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

3 ВВЕДЕНИЕ Следовательно, применяя метод индуктивных утверждений, нужно четко представлять порядок выполнения программы, чтобы быть уверенным, что не пропущен ни один из замкнутых путей в программе. Именно этот вопрос мы и рассмотрим здесь, так как сам метод утверждений мы уже описали выше, а его использование в данном случае аналогично использованию для блок-схем. Далее метод проиллюстрирован на простых программах, написанных на Фортране, на ПЛ/1 и т.п. 3 Доказательства правильности программ

4 Примеры доказательства правильности программ на Фортране ПРИМЕР 1. READ (5, 1) J1, J2 (Операторы READ… FORMAT производят ввод 1FORMAT (2I10) информации по соотвнтствующему формату) СЗНАЧЕНИЯ, СЧИТЫВАЕМЫЕ В J1 И J2 –ЦЕЛЫЕ, СУДОВЛЕТВОРЯЮЩИЕ УСЛОВИЯМ 0.LE.J1 И 1.LE.J2. IQ=0 (логические операции: LE – ; LT – < IR=J1 EQ – =; GE – 2 IF(IR.LT.J2) GO TO 4 GT – >; NE – СJ1.EQ. IQ * J2 + IR AND 0.LE. IR IQ=IQ+1 IR=IR–J2 3GO TO 2 (C – признак комментария) 4WRITE (6,5) IQ, IR (Операторы WRITE … FORMAT производят вывод 5 FORMAT (2I10) информации по соответствующему формату) СJ1.EQ. IQ*J2 + IR AND 0.LE. IR AND С IR.LT. J2 STOP END 4

5 Примеры доказательства правильности программ на Фортране Приведенная программа на Фортране – это просто некоторый вариант программы, блок-схема которой рассматривалась на лекции 2. Напомним, что программа вычисляет целое частное IQ и остаток IR от деления целого J1 на целое J2. 5

6 Примеры доказательства правильности программ на Фортране Мы уже включили в качестве комментариев в программу индуктивные утверждения, необходимые для доказательства частичной правильности. Например, комментарий, помещенный сразу после оператора с меткой 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, утверждение справедливо. 6

7 Примеры доказательства правильности программ на Фортране 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. 7

8 Примеры доказательства правильности программ на Фортране 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 станет справедливым и мы выйдем из цикла, т. е. программа закончится. 8

9 Примеры доказательства правильности программ на Фортране ПРИМЕР 2. С1Х – ВЕЩЕСТВЕННЫЙ МАССИВ, ЕГО РАЗМЕР С1N.GE. 2 XSMLST = X(1) DO 10 I = 2, N C2XSMLST РАВНО МИНИМАЛЬНОМУ ИЗ Х(1),..., Х(I – 1) С2КРОМЕ ТОГО, 2.LE. I И I.LE. N IF (XSMLST.LE. X(I)) GO TO 10 XSMLST = X(I) C3XSMLST РАВНО МИНИМАЛЬНОМУ Х(1),..., X(I – 1) C3КРОМЕ ТОГО, 3.LE. I И I.LE. N CONTINUE C4XSMLST РАВНО МИНИМАЛЬНОМУ ИЗ Х(1),..., X(N) Предполагается, что приведенный фрагмент программы должен присвоить XSMLST значение наименьшего элемента из массива Х(1),..., X(N). 9

10 Примеры доказательства правильности программ на Фортране В Фортране цикл строится по следующей основной схеме: DO метка I = M, N СПРИМЕЧАНИЕ 1 Тело цикла СПРИМЕЧАНИЕ 2 метка CONTINUE Примечание 1 (комментарий), связанное с таким циклом и стоящее непосредственно за оператором DO, нужно рассматривать как связанное с некоторой точкой утверждение 1 на блок-схеме, а примечание 2, стоящее перед концом цикла, нужно рассматривать как утверждение 2 для некоторой точки программы, соответствующей точке на блок-схеме. 10 I M тело цикла I I + 1 I N F T Утверждение 2 Утверждение 1

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

12 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 Примеры доказательства правильности программ на Фортране

13 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), что и требовалось доказать, т. е. доказана частичная правильность. Конечность этого фрагмента программы очевидна: здесь есть только один цикл, и он является фортрановским. (Заметим, что конечность фортрановского цикла, если в его теле нет переходов вне цикла, очевидно, следует считать свойством, присущим самому языку). 13 Примеры доказательства правильности программ на Фортране

14 Эти два примера показывают, что метод индуктивных утверждений можно распространить непосредственно и на доказательства правильности программ, написанных на Фортране. Затруднение заключается лишь в том, что управление в программах на Фортране не такое явное, как в блок-схемах. Это приводит к тому, что в программах легко не заметить некоторые пути или неправильно их интерпретировать (например, можно предположить, что в операторе цикла проверка выполняется перед выполнением тела цикла). Кроме того, нужно приписывание индуктивных утверждений к некоторым точкам в программе на Фортране проводить очень внимательно и все время помнить, с какой неявной точкой связано соответствующее утверждение. Например, один- единственный оператор Фортрана, такой, как оператор DO, фактически состоит из нескольких действий: установки счетчика, увеличения счетчика и проверки. 14 Примеры доказательства правильности программ на Фортране

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

16 Очень важной особенностью программирования на Фортране является возможность определять и использовать подпрограммы. Метод индуктивных утверждений мы можем распространить скорее на доказательство правильности самих подпрограмм или программ, чем на обращения к ним. Так как в предыдущих разделах, имея дело с блок-схемами, мы не касались вопроса подпрограмм, то теперь приведем пример доказательства правильности программ, содержащих обращение к подпрограммам. 16 Примеры доказательства правильности программ на Фортране

17 ПРИМЕР 3. СMAIN PROGRAM. С10.LE. I AND 1.LE. J AND A(I, J) CALL DIV(I, J, K, L) С2 0.LE. I AND 1.LE. J AND A(I, J) C2 AND I.EQ. K*J + L AND 0.LE. L AND I.LT. J. END. SUBROUTINE DIV (J1, J2, IQ, IR) C30.LE. J1 AND 1.LE. J2 IR = J1 2 IF (IR.LT. J2) GO TO 4 C4J1.EQ.IQ*J2 + IR AND 0.LE. IR IQ = IQ + 1 IR = IR – J2 3GO TO 2 4 RETURN C5 J1.EQ. IQ*J2 + IR AND 0.LE. IR AND IR.LT. J2 END 17

18 В этом примере нас прежде всего будет интересовать, как обрабатывать подпрограммы. Поэтому мы не приводим целиком основную программу, а лишь намечаем некоторую программу, содержащую обращения к подпрограммам. Подпрограмма DIV аналогична программе, приведенной в примере 1, но оформлена как подпрограмма. Она предназначена для вычисления целых частного и остатка от деления параметра J1 на параметр J2; полученные значения возвращаются как значения параметров IQ и IR. Доказательство того, что эта подпрограмма верна, аналогично доказательству, приведен­ному в примере 1. Поэтому будем считать, что доказательство правильности этой подпрограммы уже проведено, и докажем, что правильна основная программа. Один из этапов такого доказательства заключается в том, чтобы показать, что если, непосредственно перед обращением к подпрограмме справедливо утверждение С1, а затем мы пройдем эту точку, выполним подпрограмму и вернемся из нее, то будет справед­ливо утверждение С2. Мы считаем, что A(I, J) в примечаниях С1 и С2 некоторые утверждения, относящиеся к переменным I и J. Чтобы доказать этот факт, мы поступим следующим образом. Так как фактические параметры I, J, К, L с помощью механизма обращения сопоставляются с соответствующими формальными параметрами J1, J2, IQ, IR, то сначала следует доказать, что из утверждения С1 следует утверждение СЗ в начале подпрограммы; 18

19 для этого имена параметров J1, J2, IQ и IR в этом утверждении заменяются на имена соответствующих фактических параметров I, J, К, L. Другими словами, нужно доказать, что С1 подразумевает С3', где С3' – утверждение, полученное путем замены в С3 J1 на I, J2 на J, IQ на К и IR на L. Таким образом, нужно показать, что из 0.LE. I, 1.LE. J и A(I, J) следует 0.LE. I и 1.LE. J. Это очевидно. Кроме того, известно, что справедливо и на­чальное допущение о правильности параметров подпро­граммы. Так как мы считаем, что правильность подпрограммы уже доказана, то нам не надо обращать внимание на детали строения этой программы. Мы знаем, что утверждение С5, связанное с точкой, непосредственно предшествующей опера­тору RETURN, будет справедливо и после того, как мы вернемся в основную программу. Конечно, это утверждение относится к формальным параметрам, но оно будет справед­ливо и для фактических параметров после того, как мы вернемся и попадем в точку, с которой связано утверждение С2. Таким образом, для того чтобы убедиться в справедли­вости утверждения С2 при достижении соответствующей точки программы, следует лишь показать, что из С5' следует С2. Утверждение С5' получается из С5 заменой J1 на I, J2 на J, IQ на К и IR на L. Другими словами, из 1.EQ. К * J + L AND 0.LE. L AND L.LT. J следует 0.LT. I AND 1.LE. J AND A(I, J) AND I.EQ. K*J + L AND 0.LE. L AND L.LT. J. 19

20 Легко убедиться, что из С5' не следует целиком все утверждение С2, а следует лишь под­черкнутая часть С2. Как же убедиться, что оставшаяся (невыделенная) часть также справедлива, если мы попадаем в точку, соответствующую С2? Отметим, что эта часть утверж­дения идентична утверждению С2. Следовательно, если мы будем знать, что переменные I и J (в С1 упоминаются только они) в подпрограмме не изменяются, то можно сделать вывод, что из справедливости С1 перед обращением к под­ программе следует справедливость соответствующей части С2 после обращения. Так как фактические параметры I, J сопоставляются с формальными параметрами подпрограммы J1, J2, то теперь следует просмотреть подпрограмму: не изменяются ли значения J1 или J2. Студент может легко проверить, что ни J1, ни J2 не изменяются. Отсюда мы делаем вывод, что утверждение 0.LE. I AND 1.LE. J AND A(I, J) продолжает оставаться справедливым и в момент достижения точки, связанной с утверждением С2. 20

21 Приведенное доказательство иллюстрирует общий метод доказательства для случаев с подпрограммами. 1.Сначала выясняется, что делается в подпрограмме по предположению, и это доказывается обычным методом индуктивных утверждений. 2.Далее при доказательстве правильности программы, обращающейся к этой или еще и другим подпрограммам (если некоторый путь содержит такое обращение), поступаем следующим образом. 2.1.Сначала доказываем, что при обращении к подпрограмме справедливо утверждение, относящееся к ее началу (здесь описываются допущения, касаю- щиеся значений параметров). В примере мы показывали, что из С1 следует С3' Затем доказываем, что из утверждения, связанного с оператором возврата (это утверждение о правильности подпрограммы), следует справедливость всего (или части) утверждения, относящегося к точке (в вызывающей программе), непосредственно следующей за обращением. В примере мы показали, что из С5 следует часть С Кроме этого, можно использовать и тот факт, что утверждения, относящи- еся к переменным, значения которых не изменяются в подпрограмме, про- должают оставаться справедливыми и после возврата из подпрограммы. В примере показано, что из С1 следует оставшаяся часть С2 (С1 – утверждение в вызывающей программе, включающее лишь переменные, значения которых в подпрограмме не изменились). 21

22 22 Примеры доказательства правильности программ на ПЛ/1 Как для программ на Фортране, так и для программ на языке ПЛ/1 метод доказательства правильности в принципе один и тот же, однако мы хотели бы показать, как на этом методе отражаются механизмы управления, присущие ПЛ/1. ПРИМЕР 1 /*Х(1: N) МАССИВ ВЕЩЕСТВЕННЫХ ЗНАЧЕНИЙ РАЗМЕРОМ 1 N */ SUM = 0.0; I = 1; DO WHILE (I N); /*SUM = X(1) X(I – 1) AND 1 I N+1 */ SUM = SUM + X(I); I = I + 1; END; /*SUM = X(1) X(N) */

23 23 Примеры доказательства правильности программ на ПЛ/1 Предполагается, что приведенный фрагмент программы вычисляет SUM = Х(1) X(N). Вычисления организуются на основе цикла DO WHILE. Эта конструкция означает, что повторяется нуль или более раз выполнение всех операторов, расположенных между оператором DO WHILE и соответствующим ему оператором END, до тех пор, пока условие в операторе DO WHILE истинно. Утверждение, записанное в форме примечания сразу же за оператором DO WHILE, следует считать связанным с точкой, непосредственно предшествующей проверке в этом операторе, т. е. считается, что оно должно быть справедливым каждый раз, когда мы попадаем в эту точку. Доказательство частичной правильности для этой простой программы довольно очевидно. Для этого нужно просмотреть все пути в программе.

24 24 Примеры доказательства правильности программ на ПЛ/1 1. Путь от начала фрагмента программы до точки, непосре- дственно предшествующей проверке в операторе DO WHILE. Когда мы попадем в эту точку, будем иметь SUM = 0.0 и I=1. Утверждение, что SUM =Х(1)+...+ Х(I–1), очевидно справедливо, так как I – 1 = 0, и мы считаем, что «пустая» сумма равна нулю. Утверждение 1 I < N + 1 также справедливо, ибо I = 0 и N Путь от проверки в операторе DO WHILE через тело цикла вновь к проверке в операторе DO WHILE. Предположим, что до прохода по этому пути I = I N и справедливо указанное утвержде- ние, т. е. I N N + 1 и SUM = X(1) X(I N – 1). После того как мы пройдем по нашему пути, получим SUM = [X(1) X(I N – 1)] + X(I N ) и I = I N + 1. Следовательно, опять справедливо утверждение SUM = Х(1) Х(I – 1). Но мы проходим по этому пути лишь в случае истинности условия I N N. Таким образом, когда мы вернемся в точку проверки в операторе DO WHILE, будем снова иметь 1 I N + 1 = I N + 1.

25 25 Примеры доказательства правильности программ на ПЛ/1 3. Путь от проверки е операторе DO WHILE до точки, располо- женной сразу же после конца цикла. По этому пути мы проходим, если условие в операторе DO WHILE ложно, т. е. I N дает ответ «ложь». Если при этом учесть, что иметь 1 I N + 1, то очевидно, что I = N + 1. Из этого факта, а также из справедливости утверждения SUM = X(1) Х(I – 1) следует, что при достижении точки сразу же после цикла DO WHILE SUM = X(1) X((N + 1) – 1) = X(1) X(N), что и требовалось доказать. Для доказательства конечности программы нужно только показать, что заканчивается сам цикл. Это, однако, очевидно, так как I увеличивается на 1 каждый раз при прохождении цикла, а значение N не изменяется. Следовательно, I в неко­торый момент станет больше N, и проверка I N даст отрицательный результат.

26 26 Примеры доказательства правильности программ на ПЛ/1 ПРИМЕР 2 /* M, N УЖЕ ИМЕЮТ ЦЕЛЫЕ ЗНАЧЕНИЯ И 0 N */ 1 = 1; J=M; K=N; DO WHILE (K 0); /* (I*(J**K) = M**N AND 0 K */ DO WHILE (MOD (K, 2) = 0); /* I*(J**К) = M**N AND 0 < K */ K = K/2E0; J = J*J; END; K = K – 1; I = I*J; END; /* I = M**N */ Мы хотим доказать, что приведенная программа на языке ПЛ/1 вычисляет I=M**N.

27 27 Примеры доказательства правильности программ на ПЛ/1 Мы хотим доказать, что приведенная программа на языке ПЛ/1 вычисляет I=M**N. Для доказательства частичной правильности нашего фрагмента рассмотрим следующие пути в программе: 1. Пусть от начала программы до точки, предшествующей непосредственно проверке во внешнем операторе DO WHILE. Когда мы попадем в эту точку, будем иметь I = 1, J = M и K = N. Таким образом, I*(J**K) = 1*(M**N)= = M**N, кроме того, 0 N = К. Следовательно, утверждение, связанное с точкой, предшествующей проверке во внешнем операторе DO WHILE, справедливо. 2. Путь от проверки во внешнем цикле до проверки во внутреннем цикле. На этом пути выясняется лишь, что К 0. Следовательно, связанное с внутренним оператором DO WHILE утверждение должно быть справедливым.

28 28 Примеры доказательства правильности программ на ПЛ/1 3. Путь от проверки во внутреннем операторе DO WHILE по внутреннему циклу с возвратом к проверке во внутреннем операторе DO WHILE. Предположим, что до прохода по этому пути I = I N, J = J N и К = К N. Кроме того, мы знаем, что I N *( J N **K N ) = M**N и 0 < К N. Так как мы проходим по этому пути, то, следовательно, MOD (K N, 2)=0, т. е. К N без остатка делится на 2. Пройдя по телу цикла, мы получим I = I N, К = К N /2Е0 и J = J N *J N. Следовательно, I*(J**K) = I N *[(J N * J N )**K N /2E0] = = I N *(J N ** K N /2E0)*(J N **K N /2E0) = = I N * (J N ** (K N /2E0 + K N /2E0) = I N * (J N ** K N ) = M**N так как K N делится без остатка на 2. Кроме того, так как 0 0. Таким образом, утверждение, относящееся к внутреннему оператору DO WHILE, в момент возврата к нему должно быть справедливо.

29 29 Примеры доказательства правильности программ на ПЛ/1 4. Путь от проверки во внутреннем операторе DO WHILE к окончанию внешнего цикла и возврат к проверке во внешнем операторе DO WHILE. Предположим, что мы находимся во внутреннем операторе DO WHILE, I = I N, J = J N и К = К N. В этот момент справедливы утверждения I N *(J N **K N ) = = M**N и 0 < К N. Кроме того, если мы проходим по указанному пути, проверка во внутреннем DO WHILE дает отрицательный ответ, т. е. условие MOD(K N, 2) = 0 ложно. Пройдем до конца внешний цикл и вернемся к проверке во внешнем операторе DO WHILE. Теперь будем иметь К = K N – 1, I = I N * J N и J = J N. Следовательно, в этот момент I*(J**K) = (I N * J N )*[J N ** (K N – L)] = I N *[J N *( J N **(K N – L))] = = I N *[J N **(1 + K N – 1)] = I N *(J N ** K N ) = M**N. Кроме того, так как 0 < К N, то 0 < К N – 1 = К. Таким образом, связанное с внешним оператором DO WHILE утверждение снова оказывается справедливым.

30 30 Примеры доказательства правильности программ на ПЛ/1 Теперь рассмотрим внешний цикл. Отметим, что при каждом прохождении по внешнему циклу значение К уменьшается по крайней мере на 1. Действительно, если при этом мы проходим несколько раз внутренний цикл, то К уменьшается на соответ- ствующую степень 2. Если внутренний цикл не выполнялся, то перед выходом из внешнего цикла значение К стало равным К – L. Таким образом, в любом случае значение К уменьшилось по крайней мере на 1. Так как известно, что 0 К, то значение К в конце концов станет равным 0. В этот момент условие К = 0 будет истинным, и внешний цикл закончится.

31 31 Примеры доказательства правильности программ на ПЛ/1 5. Путь от проверки во внешнем операторе DO WHILE дo точки, расположенной непосредственно после конца внешнего цикла. Если мы прошли этим путем, условие К 0 было ложным, т. е. К = 0. Утверждение, соответствующее внешнему циклу, спра- ведливо, т. е. I*(J**K) = M**N. Однако, поскольку мы вышли из цикла, I*(J**K) =I*(J**0) = I*(1) = I = M**N, что и требовалось док. Для доказательства выполнения данной программы нужно показать, что если мы попадем во внешний или внутренний цикл, то эти циклы обязательно закончатся. Сначала рассмот­рим внутренний цикл. Отметим, что при каждом прохождении цикла значение К устанавливается равным К/2Е0, т. е. К все время уменьшается. Следовательно, в какой-то момент его значение уменьшится настолько, что не будет без остатка делиться на 2 В этот момент условие MOD(K, 2) = 0 станет ложным, что и гарантирует окончание внутреннего цикла. Теперь рассмотрим внешний цикл. Отметим, что при каждом прохождении по внешнему циклу значение К уменьшается по крайней мере на 1. Действительно, если при этом мы проходим несколько раз внутренний цикл, то К уменьшается на соответствующую степень 2. Если внутренний цикл не выполнялся, то перед выходом из внешнего цикла значение К стало равным К – L Таким образом, в любом случае значе­ние К уменьшилось по крайней мере на 1. Так как известно, что 0 К, то значение К в конце концов станет равным 0. В этот момент условие К = 0 будет истинным, и внешний цикл закончится.

32 32 Доказательство частичной правильности как часть процесса программирования Все примеры доказательства правильности в этом учебном курсе относились к законченным и небольшим программам. Однако на практике такое доказательство должно проводиться программистом во время самого процесса программирования. Не следует ожидать, что кто-нибудь возьмет большую, законченную программу и начнет доказывать ее правильность. Интеллектуальные затраты на такую работу были бы, вероятно, очень велики. Нужно доказывать правильность небольших фрагментов по мере того, как они составляются. Для того чтобы это можно было делать, такие секции (фрагменты) не должны вместе образовывать запутанный клубок, где не найдешь ни конца, ни начала каждой.

33 33 Доказательство частичной правильности как часть процесса программирования Многие утверждают, что программист сможет избежать излишних необходимых усложнений и запутанных структур, если он не будет использовать переходы GO TO и ограничит себя небольшим мно- жеством операторов управления с одним входом и одним выходом. Такими операторами могут быть: последовательное выполнение, условное выполнение (ветвление) вида IF С THEN SI ELSE S2 и итеративная конструкция основного вида WHILE С DO S. Программы, написанные в таком стиле, часто называют «структурированными» программами. Тем не менее использование такого ограниченного подмножества операторов управления, конечно, не спасает програм- миста от всех «болезней». И с такими операторами управления, как и с оператором GO TO, можно написать «мрачную» программу, кото- рую трудно понять и верифицировать. Важно, чтобы программа бы- ла ясна по замыслу и при этом не использовались такие операторы управления, которые запутывают связи между отдельными частями (путем переходов вперед или назад с использованием оператора GO TO). Доказывая правильность больших частей программы, многие из подчастей которой уже доказаны, можно такие подчасти трактовать как отдельные абстрактные операторы. Выполнение таких операторов будет приводить к справедли­вости некоторых постусловий (утверждений о правильности такой подчасти) при условии, что до выполнения были справедливы предусловия (входные утверждения для этой подчасти). Таким образом, доказывая правильность большого фрагмента, вовсе нет необходимости разбираться во всех его частях. Часто процесс идет в обратном порядке, т. е. про­граммист, работая по принципу «сверху вниз», составляет большой фрагмент, оставляя неопределенным в данный момент некоторые его части. Доказывая правильность этого фрагмента, он исходит из того, что упомянутые части будут написаны так, что их выполнение будет приводить к справед­ливости некоторых постусловий, если до их выполнения были справедливы предусловия. После этого, опираясь на эти утверждения, доказывается правильность большого фраг­мента. Позже, при составлении программ для более мелких частей, для доказательства их правильности нужно лишь показать, что из допущения справедливоети до их выполнения предусловий следует справедливость после выполнения постусловий. Как уже говорилось в п. 2.5, мы не считаем, что программисту необходимо выписывать все пункты дока­зательства правильности. Однако он должен выписывать все ключевые утверждения (как примечания), а затем удосто­веряться в их справедливости (без деталей). Программист должен (без лишних подробностей) удостовериться и в том, что программа в конце концов закончит работу. Основная мысль этого раздела заключается в том, что не­ формальное доказательство правильности следует проводить в процессе программирования, а не после того, как программа написана.

34 34 Доказательство частичной правильности как часть процесса программирования Доказывая правильность больших частей программы, многие из подчастей которой уже доказаны, можно такие подчасти трак- товать как отдельные абстрактные операторы. Выполнение таких операторов будет приводить к справедливости некоторых постусловий (утверждений о правильности такой подчасти) при условии, что до выполнения были справедливы предусловия (входные утверждения для этой подчасти). Таким образом, доказывая правильность большого фрагмента, вовсе нет необходимости разбираться во всех его частях. Часто процесс идет в обратном порядке, т. е. программист, работая по принципу «сверху вниз», составляет большой фрагмент, оставляя неопределенным в данный момент некоторые его части.

35 35 Доказательство частичной правильности как часть процесса программирования Доказывая правильность этого фрагмента, он исходит из того, что упомянутые части будут написаны так, что их выполнение будет приводить к справедливости некоторых постусловий, если до их выполнения были справедливы предусловия. После этого, опираясь на эти утверждения, доказывается правильность большого фрагмента. Позже, при составлении программ для более мелких частей, для доказательства их правильности нужно лишь показать, что из допущения справедливости до их выполнения предусловий следует справедливость после выполнения постусловий.

36 36 Доказательство частичной правильности как часть процесса программирования Как уже говорилось раньше, мы не считаем, что программисту необходимо выписывать все пункты доказательства правильности. Однако он должен выписывать все ключевые утверждения (как примечания), а затем удостоверяться в их справедливости (без деталей). Программист должен (без лишних подробностей) удостовериться и в том, что программа в конце концов закончит работу. Основная мысль этого раздела заключается в том, что неформальное доказательство правильности следует проводить в процессе программирования, а не после того, как программа написана.