Метод индуктивных утверждений

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

Проиллюстрируем использование описанного выше подхода на следующей структуре (рис. 6.3)

Доказать, что утверждение 1 справедливо при первом попадании в точку 1 – довольно просто. Однако, доказательство того, что если мы находимся в тоске 1 и справедливо утверждение 1, то при переходе по циклу и возврате в точку 1 утверждение 1 останется справедливым неочевидно. Так как перед возвратом в точку 1 несколько раз будет выполняться внутренний цикл.

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

1 -- При каждом попадании в эту точку цикла справедливо утверждение 1

2 -- При каждом попадании в эту точку цикла справедливо утверждение 2

Рис.6.3. Пример блок-схемы с вложенными циклами

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

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

Введем два определения.

Определение 6.1. Пусть А – некоторое утверждение, описывающее предполагаемые свойства данных в программе, а С – утверждение о правильности. Будем говорить, что программа частично правильна (по отношению к А и С), если при каждом выполнении ее с данными, удовлетворяющими А, будет справедливо утверждение С при условии, что программа закончится.

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

Определение 6.2. Будем называть программу полностью правильной (по отношению к А и С), если она частично правильна (по отношению к А и С) и заканчивается при всех данных, удовлетворяющих А.

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

Для доказательства частичной правильности программы поступаем следующим образом. Связываем утверждение А с началом программы, а утверждение С с конечной точкой программы.

Далее выявим некоторые закономерности, относящиеся к значениям переменных, и свяжем соответствующие утверждения с другими точками программы. В частности, свяжем такие утверждения в одной точке в каждом из замкнутых путей в программе (циклах).

Для каждого пути в программе, ведущего из точки n, связанной с утверждением А_n, в точку n+1, связанную с утверждением А_n+1 (при условии, что на этом пути нет точек с каким-либо дополнительным утверждением), докажем, что если мы попали в точку n и справедливо утверждение А_n, а затем прошли от точки n до точки n+1, то при попадании в точку j справедливо утверждение А_n+1.

Для цикла точки n и n+1 могут быть одной и той же точкой.

Опираясь на этот подход, докажем теорему.

Теорема 6.1. Если можно выполнить все действия, предусмотренные описанным методом индуктивных утверждений для некоторой программы, то эта программа частично правильна (относительно А и С).

Доказательство.

Пусть выполнено доказательство правильности методом индуктивных утверждений. Начнем выполнение программы с начальными данными, удовлетворяющими утверждению А.

Покажем, что каждый раз, когда мы попадаем в некоторую точку программы, с которой связано определенное утверждение, данное утверждение будет справедливо. В частности, когда достигнем последней точки программы, будет справедливо утверждение С.

Доказательство проведем с помощью индукции по n - числу точек программы, через которые уже прошли (учитываются точки, связанные с некоторыми утверждениями).

1. Пусть в процессе выполнения программы мы попали в точку n=1. Нужно показать, что в этой точке утверждение справедливо. Но первая точка – это начало программы, и с ней связано утверждение о данных А. Оно справедливо по определению.

2. Пусть мы дошли до некоторой n-ой точки, с ней связано утверждение А и пусть это утверждение справедливо (гипотеза индукции). Покажем это для n+1 точки. Очевидно, что между точками n и n+1 существует некоторый путь. Так как мы уже использовали метод индуктивных утверждений, то, следовательно, и уже рассмотрели этот путь и показали, что если находимся в n-ой точке со справедливым утверждением А_n, а затем проходим из n-ой в n+1 точку, то при ее достижении будет справедливо утверждение А_n+1. Из этого факта вместе с гипотезой о справедливости утверждения А_n следует, что при попадании в n+1 точку справедливо утверждение А_n+1. Ч.т.д.

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

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

Пример 6.2. Пусть требуется доказать, что приведенная на рисунке 1 блок-схема устанавливает переменную МАХ равной максимальному значению в двумерном массиве Х.

Указанные на блок-схеме утверждения (рис.6.4) – индуктивные утверждения, необходимые для доказательства частичной правильности программы. Так как все утверждения имеют аналогичную форму и начинаются с фразы: «При достижении этой точки справедливо», то это начало фразы мы опускаем. Утверждение о конечности программы не указано на блок-схеме, поскольку доказательство этого утверждения будет проводиться отдельно от доказательства частичной правильности.

Х – массив вещественных чисел,

состоящий из M строк и N столбцов, M³1, N ³1

1 £ I £ M+1 и

MAX= Х[1,1], если I = 1;

иначе МАХ= максимальное из

значений элементов в первых I-1 строках массива Х

МАХ – максимальное

значение в массиве Х

1£ I £ M и 1 £ J £ N+1 и

МАХ=Х[1,1], если I=1, J=1;

иначе МАХ= максимальное

из значений элементов в первых I-1 строках и первых J-1 элементов в I-й строке массива Х

Рис.6.4. Блок-схема программы в примере 6.2.

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

1. Путь из точки 1 в точку 2.

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

2. Путь из точки 2 в точку 3.

Предположим, что мы находимся в точке 2 и справедливо связанное с нею утверждение. Перейдем из точки 2 в точку 3. Требуется показать, что при попадании в точку 3 будет справедливо утверждение, связанное с этой точкой. Если мы дошли до точки 3 (из точки 2), то имеем J = 1, а значение МАХ осталось неизменным. Так как N³1, 1 £ J=1 £ N+1, а значение I после точки 2 не изменилось, то 1 £ I £ M+1. Однако если мы пришли из точки 2 в точку 3, то известно, что проверка I £ M была истинной, и, комбинируя это отношение с 1 £ I £ M+1, получаем 1 £ I £ M. Если I = 1 и J = 1, то из утверждения 2 получим МАХ = Х[1,1]. В противном случае (т.е. при I ¹1) из утверждения 2 получаем, что МАХ равно максимальному из значений элементов в первых I – 1 строках массива Х или, более точно, максимальному из значений элементов в первых 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 < 2 £ J_n+1 = J_n +1 £ N+1. На всем пути перехода в точку 3 значение МАХ не изменялось, и известно, кроме того, что истинна проверка Х[I_n,J_n] £ MAX. Если учесть истинность утверждения о МАХ до «прохода» по указанному пути, то данное утверждение остается истинным и при возврате в точку 3 с I_n+1 = I_n и J_n+1 = J_n +1. Так как Х[I_n,J_n] £ MAX, то неизменное значение МАХ снова будет максимальным из значений элементов в первых I_n+1 – 1 = I_n – 1 строках и из значений первых J_n+1 – 1 = (J_n +1) – 1 = J_n элементов в I_n-й строке массива Х.

4. Путь из точки 3 через точки 4, 6 в точку 3.

Рассуждения для этого пути аналогичны приведенным для предыдущего пути, за исключением того, что при возврате в точку 3 МАХ будет иметь значения Х[I_n,J_n]. Кроме того, так как выбран этот путь, проверка Х[I_n,J_n] £ MAX была ложной и, следовательно, MAX < Х[I_n,J_n]. Таким образом, Х[I_n,J_n] больше максимального из значений элементов первых I_n – 1 строк и J_n -1 элементов в I_n-й строке. Отсюда следует, что при возврате в точку 3 значение МАХ остается максимальным из значений элементов первых I_n+1 – 1 = I_n – 1 и первых J_n+1 – 1 = (J_n +1) – 1 = J_n элементов в I_n+1 = I_n-й строке массива Х.

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

6. Путь от точки 2 в точку 8.

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

Таким образом, мы доказали частичную правильность программы. Осталось еще удостовериться, что программа закончится. Отметим, что единственными местами в программе, где изменяются 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 станет больше значения М. В этот момент мы перейдем из точки 2 в точку 8, и программа закончится. Таким образом, доказана конечность представленной программы. Если это доказательство объединить с предыдущем доказательством частичной правильности, то из этого последует и полная правильность программы.

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

Предлагается генерировать инварианты непосредственно по тексту программы и использовать их как для доказательства корректности компонент программы, так и для проверки ее завершаемости.

В настоящее время проводятся работы по созданию автоматизированных верификаторов программ, написанных на различных языках программирования.

РЕКОМЕНДУЕМАЯ ЛИТЕРАТУРА

1. Автоматное управление асинхронными процессами в ЭВМ и дискретных системах./ Под ред. В.И.Варшавского. - М.: Наука, 1986. – 256 с.

2. Питерсон Дж. Теория сетей Петри и моделирование систем. - М.: Наука, 1984. – 264 с.

3. Гордеев А.В. Системное программное обеспечение: Учеб./Гордеев А.В., Молчанов А.Ю.- СПб.: Питер, 2001. – 736 с.

4. Дейкстра Э. Взаимодействие последовательных процессов // Языки программирования (под ред.Ф.Женюи). М.: Мир, 1972. С. 9 – 86.

5. Дейтл Г. Введение в операционные системы. В двух томах /Пер. с англ. Л. А. Теплицкого, А. Б. Ходулева, Вс. С. Штаркмана под редакцией Вс. С. Штаркмана. – М.: Мир, 1987. – 876 с.

6. Хоар Ч. Взаимодействующие последовательные процессы. – М.: Мир, 1989. – 264 с.

7. Котов В.Е. Введение в теорию схем программ. - Новосибирск: Наука, 1978. – 256 с.

8. Котов В. Е., Сабельфельд В. К. Теория схем программ Новосибирск: Наука, 1978. – 225 с.

9. Непомнящий В.А., Рякин О.М. Прикладные методы верификации программ/ Под ред. А.П.Ершова. – М.: Радио и связь, 1992. – 256 с.

10. Андерсон Р. Доказательство правильности программ: Пер.с англ. –М.: Мир, 1982. – 163 с.