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

2. Рассмотрите блок-схему, приведенную на рис. 5.3, сформулируйте и запишите индуктивные утверждения с помощью нотации исчисления предикатов и сформулируйте множество условий верификации.

       Рис. 5.2        Рис. 5.3

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

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

5. Постройте блок-схему программы для поиска максимального значения в массиве вещественных чисел X1, X2, ..., XN  размером N ≥ 1. Исходное допущение: все элементы массива уже имеют начальные значения. Сформулируйте и запишите для нее индуктивные утверждения в нотации исчисления предикатов и постройте условия верификации.

6. Постройте блок-схему программы для вычисления суммы всех положительных элементов SUMPOS и суммы всех отрицательных элементов SUMNEG в массиве X1, X2, ..., XN  (N ≥ 1) вещественных чисел. Сформулируйте и запишите для нее индуктивные утверждения в нотации исчисления предикатов и постройте условия верификации.

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

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

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

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

Тема 6. АКСИОМАТИЧЕСКИЙ ПОДХОД
К ДОКАЗАТЕЛЬСТВУ ЧАСТИЧНОЙ ПРАВИЛЬНОСТИ

Доказательство правильности для программ, написанных на языках программирования, можно производить так же, как и для блок-схем, используя метод индуктивных утверждений. А именно, сопоставить с некоторыми ключевыми точками в программе индуктивные утверждения и показать, что при попадании в процессе вычислений в ту или иную точку оказывалось справедливым соответствующее утверждение. Однако такое доказательство частичной правильности можно провести и в другой форме. Можно показать, что доказательство основывается на некоторых аксиомах или правилах верификации. Ниже рассмотрим несколько правил верификации и покажем их эквивалентность методу индуктивных утверждений. Для записи правил верификации используем следующую нотацию: {А1} Р {А2}, где А1 и А2 – утверждения (индуктивные), а Р – фрагмент программы из одного или нескольких операторов. Такая запись означает, что, если непосредственно перед выполнением Р справедливо А1, то после выполнения Р (если оно закончится) будет справедливо А2. Теперь перейдем к примерам правил верификации.

Пример 6. Представим себе, что в используемом нами языке есть оператор вида IF С ТНЕN S1 ЕLSЕ S2 и мы хотим доказать (как часть некоторого доказательства правильности), что {А1} IF С ТНЕN S1 ЕLSЕ S2 {А2}. Другими словами, нужно доказать, что, если непосредственно перед выполнением этого оператора было справедливо А1, а затем закончилось выполнение оператора, то непосредственно после этого будет справедлива А2. Мы предполагаем, что оператор имеет смысл, традиционный для языков программирования, т. е. он эквивалентен приведенному на рис. 6.1 фрагменту блок-схемы.

Аксиома, или правило верификации, которое можно использовать для доказательства приведенного утверждения, гласит:

Если можно доказать, что

1)  {А1 Λ С} S1{А2}

и

2)  {А1 Λ ¬ С} S2{А2},

то отсюда можно заключить, что

3) {А1} IF С ТНЕN S1 ЕLSЕ S2 {А2}.

Эквивалентность этой аксиомы методу индуктивных утверждений в форме, приведенной в первой части пособия, довольно очевидна. Доказательство этого факта приведено в [2, 3]. Причем необходимо заметить, что аксиоматический подход, как и метод индуктивных утверждений, используется лишь для доказательства частичной правильности. Оба варианта не гарантируют, что программа когда-нибудь закончится.

Упражнения

1. Предположим, что мы используем язык, в котором есть оператор вида

DO  WHILE  (C)

S

END;

Смысл этого оператора полностью характеризуется приведенным на рис. 6.2 фрагментом блок-схемы. Сформулируйте правила верификации для доказательства {А1} Р {А2}, где Р – такой же цикл, как DО WHILE.

2. Введем еще одно дополнительное правило верификации. Предположим, что Р1, Р2 – два фрагмента программы и необходимо доказать некоторый факт, касающийся фрагмента, состоящего из Р1, за которым непосредственно следует Р2. В этом случае если можно доказать, что

1)        {А1}  Р1  {А2}  и  2)        {А2} Р2 {А3} ,

то отсюда можно заключить, что

3)        {А1} Р1; Р2 {А3} .

Докажите с помощью правил верификации частичную правильность программы на ПЛ/1, соответствующей блок-схеме (рис. 4.1), доказательство частичной правильности методом индуктивных утверждений которой рассмотрено в примере 4. (Затем можно сравнить эти два доказательства и убедиться в их идентичности). Фрагмент программы имеет вид

/*  {0 ≤ J1 Λ 1 ≤ J2} */

IQ=0;

IR=J1;

/*  {J1= IQ ●J2 + IR  Λ  0 ≤ IR}  */

DО WHILE (IR ≥ J1);

IQ = IQ + 1;

IR = IR – J2;

END ;

/*  {J1= IQ ●J2 + IR  Λ  0 ≤ IR < J2}  */

Требуется доказать, что {0 ≤ J1 Λ 1 ≤ J2}, P {J1= IQ ●J2 + IR Λ 0 ≤ IR < J2}, где Р – приведенный выше фрагмент программы.

3. Представьте, что в используемом языке программирования есть оператор вида IF C THEN S и нужно доказать, что {А1} IF C THEN S {А2}. Сформулируйте правило верификации для этого случая.

4. Представьте, что в используемом языке программирования есть оператор вида REPEAT S UNTIL С. Этот оператор имеет традиционный для языков программирования смысл: он эквивалентен приведенной на рис. 6.3 блок-схеме. Сформулируйте правило верификации для доказательства справедливости {А1} REPEAT S UNTIL С{А2}.

5. Предположим, что нужно доказать правильность программного фрагмента:

{А1}

DО WHILE (С1);

IF C THEN S1 ELSE S2;

END;

{А2}.

Сформулируйте правила верификации, которые необходимо для этого доказывать.

6. С помощью правил верификации докажите частичную правильность следующего фрагмента программы на языке ПЛ/1:

/*  {0 < N}  */

I = 0;

J = 1;

DО WHILE (I < N);

J = J * M;

I = I + 1;

END ;

/*  {J = M ** N}  */

Тема 7. РЕКУРСИВНЫЕ ПРОГРАММЫ

Рекурсивными называются программы, в которых при вычислениях допускается обращение (рекурсивное) к самой себе аналогично тому, как обычная, нерекурсивная программа обращается к некоторой подпрограмме. Рекурсия разрешается во многих языках программирования. Рекурсивные программы особенно удобны в тех случаях, когда речь идет о данных, структура которых определяется рекурсивно (например, списки или деревья). В языке Лисп, созданном специально для «нечисленных» вычислений на основе списков, понятие рекурсии является фундаментальным. Основной метод при доказательстве правильности рекурсивных программ называется методом структурной индукции. Доказательство методом структурной индукции представляет собой доказательство с помощью математической индукции, но индукция осуществляется по структуре данных, с которыми работает программа.

Введение понятие рекурсии

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

F(Х1, ... , ХN) ≡ IF  проверка 1  THEN  выражение 1

       ELSE IF  проверка 2  THEN  выражение 2

       .

       :

       ELSE IF  проверка m  THEN  выражение m

       ELSE  OTHERWISE  выражение m + 1

Такая программа вычисляет значение F(Х1,... , ХN). Сначала выполняется проверка 1. Если проверка 1 дает ответ «истина», то значение функции есть значение выражения 1. Если проверка 1 дает ответ «ложь», то выполняется проверка 2. Если эта проверка дает ответ «истина», то значение функции есть значение выражения 2. Процесс идет таким образом до тех пор, пока не будет обнаружена первая из проверок (i-я), дающая значение «истина». Значение функции в этом случае есть значение выражения i. Если ни одна из проверок не окажется положительной, то значение функции есть значение выражения m + 1. Рекурсия вводится в этот язык программирования следующим образом: функция F, определяемая в нашей программе, может входить как часть в любое из выра­жений или проверок в программе. Такое появление F называется рекурсивным обращением к этой функции. Для каждой такой рекурсивной программы нужно еще указать, для каких значений аргументов X1, ... , ХN применима программа, т. е. нужно задать область определения функции. Выполнение программы заключается в применении ее к некоторым конкретным данным из ее области определения.