Сборник задач по курсу «Теория вычислительных процессов» (стр. 6 )

       4                WRITE (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.1. (Правильность этой блок-схемы доказана в [1]). Программа вычисляет целое частное IQ и остаток IR от деления целого J1 на целое J2. Мы уже включили в качестве комментариев в программу индуктивные утверждения, необходимые для доказательства правильности. Например, комментарий, помещенный сразу после оператора с меткой 2, нужно рассматривать как коммен­тарий, связанный с точкой, расположенной перед выполня­емой в этом операторе проверкой. Таким образом, предпо­лагается, что в момент прихода в точку, находящуюся непо­средственно перед проверкой в операторе с меткой 2, спра­ведливы утверждения J1 = IQ⋅ J2 + IR и 0 ≤ IR. Отметим, что в доказательствах мы используем « = » как символ равенства, а не присваивания.

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

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

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 до выполнения цикла принимают значения IQn и IRn. Тогда J1 =IQn ∙ J2 + IRn и 0 ≤ IRn. При возврате к метке 2 после прохождения цикла значения IQ и IR будут IQn+1 = IQn + 1 и
IRn+1 = IRn – J2, а значения J1 и J2 останутся без изменений. Таким образом, после возврата к метке 2 имеем

IQn+1 ∙ J2 + IRn+1 = (IQ + 1)⋅ J2 + (IRn – J2) =

= IQn ⋅J2 + J2 + IRn – J2 = IQn ∙ J2 + IRn = J1.

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

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

Упражнения

1. На одном из языков программирования напишите программу вычисления произведения M на N при условии, что знак умножения использовать нельзя, M и N имеют целые значения и M ≥ 0 (блок-схема программы приведена на рис. 2.3). Докажите правильность написанной программы.

2. На одном из языков программирования напишите программу вычисления и печати значения M N при условии, что M и N имеют целые значения и M ≥ 1, N ≥ 1, (блок-схема программы приведена на рис. 2.4). Докажите правильность написанной программы.

3. На одном из языков программирования напишите программу вычисления и печати значения M! = 1 ⋅ 2 ⋅ 3 ⋅ ... ⋅ (M – 1) ⋅ M при условии, что в качестве M вводится положительное целое, (блок-схема программы приведена на рис. 2.5). Докажите правильность написанной программы.

4. Докажите правильность программного фрагмента, считая, что он присваивает переменной XSMLST значение наименьшего элемента массива X(N).

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

               XSMLST = X(1)

               DO 10  I = 2, N

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

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

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

                       XSMLST = X(I)

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

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

       10        CONTINUE

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

Замечание: в Фортране цикл строится по следующей основной схеме, приведенной на рис. 4.2, которая работает аналогично приведенной на рис. 4.3 блок-схеме.

       DO метка I = M, N

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

       Тело цикла

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

  метка        CONTINUE

       Рис. 4.2        Рис. 4.3

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

5. На языке Си напишите программу поиска минимального элемента одномерного массива, соответствующую программе задачи 4, написанной на языке Фортран. Расставьте индуктивные утверждения и докажите правильность написанной программы.

6. На языке Си напишите программу вычисления целого частного IQ и остатка IR от деления целого J1 на целое J2, соответствующую программе примера 1, написанной на языке Фортран, и блок-схеме на рис. 4.1. Расставьте индуктивные утверждения и докажите правильность написанной программы.

7. На одном из языков программирования напишите программу вычисления значения определенного интеграла по формуле (считая Δt = (q – p) / (n – 1))

и докажите ее правильность.

8. На одном из языков программирования напишите программу вычисления значения функции f(x)=3 sin x для х=π/2, используя для вычисления приближенные выражения с точностью ε=0,1. (Суммирование членов ряда прекратить, если очередной член ряда, прибавляемый к сумме, будет меньше ε). Расставьте индуктивные утверждения и докажите правильность написанной программы.

9. На одном из языков программирования напишите программу вычисления суммы членов ряда  с точностью ε = 0,1. (Суммирование членов ряда прекратить, если очередной член ряда, прибавляемый к сумме, будет меньше ε). Расставьте индуктивные утверждения и докажите правильность программы.

10. На одном из языков программирования напишите программу вычисления суммы членов ряда  с точностью ε=0,1, но вычисление факториала оформите в виде подпрограммы. Докажите правильность программы.

11. На одном из языков программирования напишите программу вычисления суммы элементов двумерного массива AM×N и докажите ее правильность.

12. На одном из языков программирования напишите программу вычисления суммы элементов двумерного массива AM×N, но вычисление суммы элементов каждого столбца матрицы оформите в виде подпрограммы. Докажите правильность написанных программ.

13. На одном из языков программирования напишите программу вычисления наибольшего произведения элементов строк матрицы AM×N. Рекомендация: постройте блок-схему, расставьте индуктивные утверждения на блок-схеме, а затем введите их в текст программы в качестве комментариев и докажите правильность написанной программы.