Задания для самостоятельной работы

⇐ ПредыдущаяСтр 6 из 8Следующая ⇒

1. Докажите, что программа (рис. 8) вычисляет и печатает значение
M! = 1 × 2 × 3 × ... × (M – 1) × M при условии, что M – положительное целое число.

2. Докажите, что если в программу (рис. 9) в качестве значений I и J вводятся I₀ и J₀, причем 0 £ I₀, то печатаемые в конце значения I и J будут 0 и J₀ + 2 × I₀.

3. Постройте блок-схему алгоритма подсчета количества отрицательных элементов в матрице A_M_´_N (M, N ³ 1), содержащей целые числа, и докажите ее правильность методом индуктивных утверждений.

2.4. Контрольные вопросы к защите Лабораторной работы №2
Тема1 «Доказательство правильности блок-схем», Тема2
«Доказательство правильности блок-схем методом индуктивных утверждений»

1. Сколько и каких индуктивных утверждений надо сформулировать для доказательства правильности блок-схем?

2. Что такое «инвариант цикла»?

3. Что называется утверждением о правильности ?

4. Что такое «утверждение о конечности цикла»?

5. Как можно получить и как можно доказать инвариант цикла?

6. Сколько и каких шагов включает доказательство правильности блок-схемы?

7. В чем заключается метод индуктивных утверждений?

8. Может ли начало и конец замкнутого пути быть одной точкой?

9. Определение частично правильной программы

10. Определение полностью правильной программы

11. В чем отличие частично правильной программы от полностью правильной?

12. Метод индуктивных утверждений доказывает частичную или полную правильность программы?

13. Для доказательства полной правильности программы метод индуктивных утверждений является необходимым или достаточным условием?

14. Какое из индуктивных утверждений (о входных данных, инвариант цикла,
о конечности цикла, о правильности) не используется в методе индуктивных утверждений и почему?

Рис. 8 Рис. 9

Глава 3. ДОКАЗАТЕЛЬСТВО ПРАВИЛЬНОСТИ ПРОГРАММ, НАПИСАННЫХ НА ОБЫЧНЫХ ЯЗЫКАХ ПРОГРАММИРОВАНИЯ

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

Метод индуктивных утверждений, о котором шла речь в предыдущей главе, можно непосредственно использовать для доказательства частичной правильности программ, написанных на каком-нибудь традиционном языке программирования, например на Фортране, Алголе или ПЛ/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. IR               GT – “>”
           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₊₁ = IQ_N + 1 и IR_N₊₁ = IR_N – J2, а значения J1 и J2 останутся без изменений. Таким образом, после возврата к метке 2 имеем

IQ_N₊₁ • J2 + IR_N₊₁ = (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₊₁.

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₊₁ = I_N + 1; следовательно, значение XSMLST снова будет равно наименьшему из Х(1), ... , Х(I_N) = Х(I_N₊₁–1). Кроме того, из примечания 2 известно, что 2 £ I_N £ N, и, следовательно, в точке 3 3 £ I_N₊₁ = 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 в программах на Фортране тоже порождает проблемы. Если в программе много переходов и при их использовании не придерживались некоторой дисциплины, то программу часто трудно понимать и трудно доказывать ее правильность. Это объясняется тем, что сложно проследить за всеми возможными путями выполнения программы и указать нужные для этих путей индуктивные утверждения. (Однако существует и иная точка зрения Если у нас есть только переходы, то программа на фортране становится полностью аналогичной блок-схеме и доказательство правильности проходит так же легко, как и для блок-схем, ибо мы «видим» все точки с утверждениями. Но переходы действительно усугубляют трудности «неявных» точек, например, в операторе цикла.

Дата добавления: 2018-05-12; просмотров: 353; Мы поможем в написании вашей работы!

Поделиться с друзьями:

⇐ Предыдущая 1 2 3 4 567 8 Следующая ⇒

Мы поможем в написании ваших работ!