Описание метода индуктивных утверждений

Для доказательства правильности программы (блок-схемы) поступим следующим образом. Свяжем утверждение A с началом программы, а утверждение С – с конечной точкой программы. Кроме этого, выявим некоторые закономерности, относящиеся к значениям переменных, и свяжем соответствующие утверждения с другими точками программы. В частности, свяжем такие утверждения по крайней мере с одной из точек в каждом из замкнутых путей в программе (в циклах). Для каждого пути в программе, ведущего из точки i, связанной с утверждением A_i, в точку j, связанную с утверждением a_j (при условии, что на этом пути нет точек с какими-либо дополнительными утверждениями), докажем, что если мы попали в точку i и справедливо утверждение А_i, а затем прошли от точки i до точки j, то при попадании в точку j будет справедливо утверждение a_j. Для циклов точки i и j могут быть одной и той же точкой.

Проиллюстрируем этот прием на примере программы, содержащих вложенные циклы.

ПРИМЕР 3. Требуется доказать, что приведенная на рис. 3.1 блок-схема устанавливает переменную XLGST равной максимальному значению в массиве X. Указанные на блок-схеме утверждения – индуктивные утверждения, необходимые для доказательства правильности программы. Утверждение о конечности программы мы не помещаем на блок-схеме, поскольку доказательство этого утверждения проводится отдельно от доказательства правильности.

Сначала надо удостовериться, что программа закончится. Отметим, что единственными местами в программе, где изменяются I и J, являются «изолированные» части двух итерационных блоков, управляющие увеличением параметра цикла. Так как значение J увеличивается на 1, а значение N при выполнении внутреннего цикла не изменяется (путь через точки 3, 4, 5, 3 или через точки 3, 4, 6, 3), то значение J должно в конце концов превысить значение N. Таким образом, попадая в точку 3, мы когда-нибудь (после конечного числа выполнений внутреннего цикла) должны попасть в точку 7, а затем в точку 2, При каждом попадании в точку 2 мы затем попадем либо в точку 8, и процесс закончится, либо в точку 3. Если мы попали в точку 3, мы только что видели, как в конце концов дойдем до точки 7 и вернемся в точку 2. При этом значение I будет увеличиваться на 1, а значение M останется неизменным. Следовательно, после конечного числа шагов значение I станет больше значения M. В этот момент мы перейдем из точки 2 в точку 8, и программа закончится. Таким образом, мы доказали конечность нашей программы.

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

1. Путь из точки 1 в точку 2. Предположим, что мы находимся в точке 1 и связанное с ней утверждение справедливо, т.е. данные удовлетворяют исходному допущению. Перейдем из точки 1 в точку 2. Нужно показать, что после прихода в точку 2 связанное с этой точкой утверждение будет справедливо. Если мы попали в точку 2 из точки 1, то имеем I = 1 и XLGST = X_1,1. Так как M³1, то очевидно, что 1 £ (I=1) £ M+1. Поскольку XLGST = X_1,1 и I=1, то утверждение о XLGST справедливо.

2. Путь из точки 2 в точку 3. Предположим, что мы находимся в точке 2 и справедливо связанное с нею утверждение. Перейдем из точки 2 в точку 3. Тре

буется показать, что при попадании в точку 3 будет справедливо утверждение, связанное с этой точкой. Если мы дошли до точки 3 (из точки 2), то имеем J = 1, а значение XLGST осталось неизменным. Так как N³1, 1 £ (J=1) £ N+1, а значение I после точки 2 не изменялось, то 1 £ I £ M + 1. Однако если мы пришли из точки 2 в точку 3, то известно, что проверка 1£M была истинной, и, комбинируя это отношение с 1 £ I £ M + 1, получаем 1 £ I £ M. Если I = 1и J = 1, то из утверждения 2 получим XLGST = X_1,1. В противном случае (т.е. при I¹1) из утверждения 2 получаем, что XLGST равно максимальному из значений элементов в первых I–1 строках массива X или, более точно, максимальному из значений элементов в первых I–1 строках и из значений первых J–1 = 1–1 = 0 элементов в I-й строке. Таким образом, очевидно, что при переходе из точки 2 в точку 3 утверждение, связанное с точкой 3, оказывается справедливым.

3. Путь из точки 3 через точки 4, 5 к точке 3. Предположим, что мы находимся в точке 3 и справедливо утверждение, связанное с этой точкой. Пройдем через точки 4, 5 к точке 3. Нужно показать, что при возврате в точку 3 соответствующее утверждение останется справедливым. Пусть I и J в исходном положении в точке 3 принимают значения I_n и J_n. Мы имеем 1 £ I_n £ M и
1 £ J_n £ N+1. При возврате в точку 3 через точки 4 и 5 получим I_n+1 = I_n и
J_n+1 = J_n + 1. Следовательно, опять имеем 1 £ I_n+1 = I_n £ M. Если мы проходим по этому пути, то проверка J_n £ N была истинной. Из этого, а также из соотношения 1 £ J_n £ N+1 получаем 1 £ J_n £ N. Таким образом, при возврате в точку 3 снова имеем 1 < (J_n+1 = J_n + 1) £ N+1. На всем пути перехода в точку 3 значение XLGST не изменялось, и известно, кроме того, что истинна проверка

£ XLGST. Если учесть истинность утверждения о XLGST до «прохода» по указанному пути, то данное утверждение остается истинным и при возврате в точку 3 с I_n+1 = I_n и J_n+1 = J_n + 1. Так как

£ XLGST, то неизменное значение XLGST снова будет максимальным из значений элементов в первых
I_n+1 – 1 = I_n– 1 строках и из значений первых J_n+1– 1 = (J_n + 1) – 1 = J_n элементов в I_n-й строке массива X.

4. Путь из точки 3 через точки 4, 6 в точку 3. Рассуждения для этого пути аналогичны приведенным для предыдущего пути, за исключением того, что при возврате в точку 3 XLGST будет иметь значения

. Кроме того, так как выбран этот путь, проверка

£ XLGST была ложной и, следовательно, XLGST <

. Таким образом,

больше максимального из значений элементов первых I_n– 1 строк и J_n – 1 элементов в I_n-й строке. Отсюда следует, что при возврате в точку 3 значение XLGST остается максимальным из значений элементов первых I_n+1 – 1 = I_n– 1 строк и первых J_n+1– 1 = (J_n + 1) – 1 = J_n элементов в I_n+1 = I_n-й строке массива X.

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

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

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

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

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

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

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

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

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

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

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

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

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

READ (5, 1) J1, J2 (Операторы READ… FORMAT производят ввод

1 FORMAT (2I10) информации по соответствующему формату)

С 0.LE.J1 И 1.LE.J2. (логические операции: LE – “ £ ”

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

4 WRITE (6,5) IQ, IR (Операторы WRITE … FORMAT производят вывод

5 FORMAT (2I10) информации по соответствующему формату)

Приведенная программа на Фортране – это некоторый вариант программы, блок-схема которой приведена на рис. 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. Таким образом,

Следовательно, наше утверждение справедливо.

2. Путь от оператора с меткой 2 до оператора с меткой 3 и опять к оператору с меткой 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_n. Отсюда следует, что при возврате к метке 2 имеем 0 £ IR_n – J2 = IR_n+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. Поиск минимального элемента одномерного массива.

5. Вычисление целого частного IQ и остатка IR от деления целого J1 на целое J2, аналогично программе примера 4, написанной на языке Фортран, и блок-схеме на рис. 4.1.

6. Вычисление значения определенного интеграла по формуле

7. Вычисление суммы членов ряда

с точностью e = 0,1. (Суммирование членов ряда прекратить, если очередной член ряда, прибавляемый к сумме, будет меньше e).

8. Вычисление суммы членов ряда

с точностью e=0,1, но вычисление факториала оформите в виде подпрограммы.

9. Вычисление суммы элементов двумерного массива A_M_´_N.

10. Вычисление суммы элементов двумерного массива A_M_´_N, но вычисление суммы элементов каждого столбца матрицы оформите в виде подпрограммы.

Тема 5. ФОРМАЛИЗАЦИЯ ДОКАЗАТЕЛЬСТВА правильности
С ПОМОЩЬЮ ИДУКТИВНЫХ УТВЕРЖДЕНИЙ

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

Напомним, что метод индуктивных утверждений состоит в следующем [1]. Для доказательства частичной правильности некоторой блок-схемы относительно утверждений А и С мы связываем утверждение А с начальной точкой блок-схемы, а утверждение С – с конечной. Кроме этого, необходимо выделить и связать с блок-схемой некоторые другие утверждения (описывающие отношения между значениями переменных, справедливые в момент попадания в соответствующую точку программы). Нужно, в частности, связать по крайней мере с одной из точек в замкнутом пути (цикле) одно такое утверждение. Затем необходимо для каждого пути в блок-схеме, ведущего из точки i с утверждением А_i в точку j с утверждение А_j при условии, что на пути из i в j нет промежуточных точек с утверждениями, доказать, что если мы находимся в точке i и справедливо утверждение А_i а затем переходим по нашему пути в точку j, то при попадании в эту точку будет справедливо утверждение А_j. Для формализации такого доказательства необходимо:

1) использовать некоторую формальную нотацию для записи утверждений;

2) формализовать то, что необходимо доказывать для каждого пути в блок-схеме;

3) использовать для выполнения доказательства некоторую формальную систему вывода (дедуктивную систему).

Мы рассмотрим лишь вопросы, относящиеся к п. 1 и 2. Для цели, указанной в п. 1, можно использовать нотацию исчисления предикатов (или другую формальную нотацию), с помощью которой можно формулировать нужные утверждения. Что касается п. 2, то надо дать некоторый систематический метод формирования для каждого из путей блок-схемы подлежащего доказательству формализованного высказывания. Множество всех таких высказываний, которые нужно доказывать для определения частичной правильности программы, иногда называют множеством условий верификации (verification conditions) для этой программы.

Для систематического формирования условий верификации некоторой блок-схемы поступим следующим образом. Рассмотрим по порядку все пути в блок-схеме и сформулируем алгоритм формирования условия верификации на пути из точки i в точку j.

1. Утверждение, относящееся к точке i, обозначим через А_i(Х, Y,...), где
X, Y,... – переменные, входящие в это утверждение. Аналогично обозначим и утверждение для точки j: А_j(Х, Y,...). По пути из точки i в точку j значения переменных могут измениться (например, оператором присваивания). Для переменной V через e_path(V) (изменение переменной вдоль пути) будем обозначать выражение, определяющее значение переменной V в точке j «в терминах» значений переменных в точке i и значений, присваиваемых переменным по мере прохождения пути. Если, например, на пути из i в j было три оператора присваивания
Х X + 1, Y Y + Y и X Х + Y – 2,

то e_path(Х) = (Х + 1) + (Y + Y) – 2 = X + 2•Y – 1, e_path(Y) = Y + Y = 2•Y.

2. На пути из точки i в точку j может встретиться несколько точек, где выполняются проверки. Будем обозначать такие проверки через t_k(Х, Y,...), где k – указывает точку, к которой относится проверка, а X, Y,... – переменные, от которых она зависит. Предположим, что t_k(Х, Y,...),..., t₁(Х, Y,...) – полный набор всех проверок, встречающихся в различных точках на пути из точки i в точку j. Для каждой из этих проверок (t_m(Х, Y,...)) сформулируем высказывание

если путь из i в j проходит по ветви, отмеченной T (истина), и

если путь из i в j проходит по ветви, отмеченной буквой F (ложь). Через path¢ обозначается часть пути из i в j от точки i до точки m.

3. Образуем полное высказывание

. Запишем формализованное условие верификации для пути из точки i в точку j:

Если на пути не встречаются проверки, то С _path высказывание не включается.

Пример 5. Рассмотрим блок-схему (рис. 5.1), с которой мы уже имели дело в примере 4 и в учебных пособиях [1, 2]. Для записи утверждений, относящихся к разным точкам блок-схемы, использована нотация исчисления предикатов. Сформируем множество условий верификации.

1. Путь из точки 1 в точку 2 назовем р1. Для этого пути имеем

Так как по пути проверки не выполняется, то можно написать следующее условие верификации для этого пути:

(0 £ J1 L 1 £ J2) ® [е_р1(J1) = е_р1(IQ) · е_р1(J2) + е_р1(IR) L 0 £ е_р1(IR)],
(0 £ J1 L 1 £ J2) ® (J1 = IQ · J2 + J1 L 0 £ J1).

2. Путь из точки 2 через точки 3, 4 в точку 2 обозначим через р2.

На пути есть только одна проверка IR < J2. Ту часть пути р2, которая ведет от точки 2 до этой проверки, обозначим через р2'. Так как путь р2 после проверки проходит по ветви, отмеченной F, то

Отсюда условие верификации для этого пути имеет вид

(J1 = IQ · J2 + IR L 0 £ IR L J2 £ IR)®
® [е_р2(J1) = е_р2(IQ) · е_р2(J2) + е_р2(IR) L 0 £ е_р2(IR)],

(J1 = IQ · J2 + IR L 0 £ IR L J2 £ IR) ® [J1 = (IQ + 1) · J2 + (IR – J2) L 0 < IR – J2].

3. Путь из точки 2 через 5 в точку 6 обозначим через рЗ.

Для этого пути имеем е_р3(J1) = J1, е_р3(J2) = J2, е_р3(IQ) = IQ, е_р3(IR) = IR. На пути встречается лишь одна проверка IR < J2.

Часть пути от точки 2 до этой проверки обозначим через р3'. Как и выше, имеем е_р3_'(IR) = IR и е_р3_'(J2) = J2. Так как после проверки путь проходит по ветви, обозначенной Т (истина), то

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

(J1 = IQ · J2 + IR L 0 £ IR L IR < J2) ® (J1 = IQ · J2 + IR L 0 < IR L IR < J2).

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

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

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

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

3. Поиск максимального значения в массиве вещественных чисел X ₁, X ₂,..., X_N размером N ³ 1. Считаем, что элементы массива уже имеют начальные значения.

4. Вычисление суммы всех положительных элементов SUMPOS и суммы всех отрицательных элементов SUMNEG в массиве X ₁, X ₂,..., X_N (N ³ 1) вещественных чисел.

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

6. Вычисление и печать суммы всех элементов массива X, состоящего из M строк и N столбцов.

7. Поиск максимального значения в массиве вещественных чисел A _M_´_N (M ³ 1, N ³ 1), считая, что все элементы массива уже имеют начальные значения.

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

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

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

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

то отсюда можно заключить, что 3) {А₁} IF С ТНЕN S1 ЕLSЕ S2 {А₂}.

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

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

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

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

Докажите с помощью правил верификации частичную правильность программы на ПЛ/1, соответствующей блок-схеме (рис. 4.1), доказательство частичной правильности методом индуктивных утверждений которой рассмотрено в примере 4. Фрагмент программы представлен на рис. 6.3. Требуется доказать, что {0 £ J1 L 1 £ J2} P {J1= IQ ·J2 + IR L 0 £ IR < J2}, где Р – приведенный выше фрагмент программы. Убедитесь в идентичности этих доказательств.

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

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

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

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

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

Что будет с Землей, если ось ее сместится на 6666 км? Что будет с Землей? - задался я вопросом...

Конфликты в семейной жизни. Как это изменить? Редкий брак и взаимоотношения существуют без конфликтов и напряженности. Через это проходят все...

Что вызывает тренды на фондовых и товарных рынках Объяснение теории грузового поезда Первые 17 лет моих рыночных исследований сводились к попыткам вычислить, когда этот...

ЧТО ПРОИСХОДИТ, КОГДА МЫ ССОРИМСЯ Не понимая различий, существующих между мужчинами и женщинами, очень легко довести дело до ссоры...

Не нашли то, что искали? Воспользуйтесь поиском гугл на сайте: