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

5. Путь из точки 3 через точку 7 в точку 2. Предполо­жим, что мы находимся в точке 3 и справедливо соответ­ствующее утверждение. Перейдем из точки 3 через точку 7 в точку 2. Нужно показать, что при возврате в точку 2 будет справедливо связанное с нею утверждение. Из точки 3 в точ­ку 7 мы попадем только тогда, когда ложна проверка J ≤ N. Но из утверждения, относящегося к точке 3, известно, что 1 ≤ J ≤ N+1. Отсюда можно заключить, что J = N+1. Пусть I в точке 3 принимает значение In. Утверждение в точке 3 гласит:
1 ≤ In  ≤ M и XLGST равно максимальному из зна­чений элементов в первых
In – 1 строках и первых J – 1 = (N + 1) – 1 = N элементов в In-й строке массива X. Но так как в массиве X существует только N столбцов, то XLGST равно максимальному из значений элементов в In строках массива X. Значение XLGST между точками 3 и 2 не изменялось, а значение I изменилось и стало равным I + 1. Так как в точке 3 было справедливо отношение 1≤ In ≤ M, то это означает, что
1 < (In+1 = In + 1) ≤ M + 1 справедливо в точке 2. Следовательно, при достижении точки 2 будет справедливо утверждение: XLGST равно максимальному из значений элементов в первых I – 1 = (In + 1) – 1 = In  строках массива X.

6. Путь от точки 2 в точку 8. Предположим, что мы находимся в точке 2, справедливо соответствующее утверж­дение и мы переходим в точку 8. Необходимо показать, что при достижении точки 8 будет справедливо связанное с нею утверждение. Из точки 2 мы перейдем в точку 8, если была ложной проверка
I ≤ M. Однако в точке 2 было справедливо неравенство 1≤ I ≤ M+ 1; следовательно, можно заключить, что I= M+1. Значение XLGST при переходе из 2 в 8 не изменялось, и, таким образом, из утверждения, относящегося к точке 2, можно заключить, что при попадании в точку 8 XLGST равно максимальному из значений эле­ментов в первых I – 1 = (M + 1) – 1 = M строках массива X. Но массив X содержит только M строк; следовательно, XLGST равно максимальному из значений элементов X.

Если объединить это доказательство с предыдущим доказательством конечности программы, то отсюда следует полная правильность программы.

Упражнения

1. Постройте блок-схему для вычисления и печати суммы всех элементов массива X, состоящего из M строк и N столбцов и докажите ее правильность.

2. Докажите, что приведенная на рис. 3.2 программа устанавливает L=0, если массивы X и Y не имеют каких-либо совпадающих значений, и L=1, если имеется по крайней мере один общий элемент.

3. Докажите, что приведенная на рис. 3.3 программа конечна (т. е. заканчивается после вывода на печать всех чисел из входного файла вместе с их факториалами. Входной файл состоит из конечного числа положительных целых чисел.

       Рис. 3.2        Рис. 3.3

4. Докажите, что выполнение приведенной на рис. 3.4 «обобщенной» блок-схемы закончится. Для этого сначала докажите, что при каждом попадании в точки 2 и 4 справедливы соответствующие утверждения. Затем, зная это, убедитесь, что если, попав в точку 4, мы переходим в точку 2, то перед этим мы конечное число раз проходили по циклу 4, 5, 4. На следующем этапе покажите, что цикл через точки 2, 4 выполняется конечное число раз, прежде чем будет справедливо отношение K = N и мы перейдем в точку 7, т. е. закончим работу.

5. Докажите, что выполнение приведенной на рис. 3.5 «обобщенной» блок-схемы закончится. Для этого сначала свяжите с точками цикла (как в упражнении 4) некоторые утверждения, относящиеся к значениям переменных, и докажите их справедливость в соответствующие моменты. Затем используйте эти факты для доказательств, относящихся к разным циклам.

       Рис. 3.4

               Рис. 3.5

6. При доказательстве конечности сложных блок-схем, содержащих несколько вложенных или «пересекающихся» циклов, очень полезно проверять, что значение некоторой переменной, определяющей конечность одного из циклов, не изменяется в каком-либо другом цикле таким образом, что это будет приводить к бесконечной работе программы. На рис. 3.6 приведена «обобщенная» блок-схема, работа которой не закончится. Объясните, почему. Если бы мы имели дело не с такой «скелетной» блок-схемой, а со схемой, содержащей большое число различных действий в циклах, то обнаружить, что некоторая переменная изменяется в различных циклах, оказалось бы значительно труднее. Отсюда следует, что доказательство конечности таких блок-схем нужно проводить весьма тщательно.

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

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

9. Постройте блок-схему программы для поиска максимального значения в массиве вещественных чисел A M×N  (M ≥ 1, N ≥ 1). Считайте, что все элементы массива уже имеют начальные значения. Докажите правильность блок-схемы.

10. Постройте блок-схему для поиска в обратном порядке в массиве A M N  (M ≥ 1, N ≥ 1).элемента, равного K (т. е. поиск начинается с A M×N и заканчивается на A 11). При завершении работы программы некоторые переменные, например J1 и J2, должны быть равны индексам первого с конца элемента массива, равного K, или же нулю, если такого элемента обнаружить не удалось. Докажите, что ваша программа правильна.

11. Постройте блок-схему программы, меняющей местами значения массивов XM×N  и YM×N (M, N ≥ 1). Докажите правильность программы.

12. Постройте блок-схему программы для вычисления суммы всех положительных элементов SUMPOS и суммы всех отрицательных элементов SUMNEG в массиве YM×N (M, N ≥ 1) вещественных чисел. Докажите правильность программы.

13. Постройте блок-схему программы, проверяющей матрицу AM×M на симметричность (установить значение переменной L= 0 если А симметрична и L=1 в противном случае). Докажите, что ваша программа правильна.

14. Постройте блок-схему программы, проверяющей массивы AM и ВN, состоящие из вещественных чисел, на совпадение элементов (установить значение переменной L=0 если есть совпадающие элементы и L=1 в противном случае). Докажите правильность программы.

15. Постройте блок-схему программы, которая в матрице AM×N (M, N ≥ 1), содержащей целые числа, заменяет отрицательные элементы их модулями. Докажите правильность программы.

16. Постройте блок-схему программы для проверки матрицы AM×M, является ли она положительноопределенной (установить значение переменной L=0 если это так, и L=1 в противном случае). Исходное допущение: все элементы массива уже имеют начальные значения. Докажите правильность блок-схемы.

17. Постройте блок-схему программы, которая в двумерном массиве AM×N (M, N ≥ 1), состоящем из вещественных чисел, подсчитывает количество элементов |ai, j| < ε, (ε=0,1) и заменяет их нулями. Докажите, правильность программы.

18. Постройте блок-схему программы, которая в массиве AM производит сортировку элементов по возрастанию.

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

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

ПРИМЕР 4. Доказать правильность программы, написанной на фортране.

       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 – признак комментария)