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

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

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

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

1. утверждение А связывают с началом программы, а утверждение С – с конечной точкой программы;

2. выявляют некоторые закономерности, относящиеся к значениям переменных, и связывают соответствующие утверждения с другими точками программы;

3. для каждого пути, ведущего из точки i, связанной с утверждением А_i, в точку j, связанную с утверждением А_j, доказывают, что если попасть в точку i и при этом будет справедливо утверждение А_i, а затем пройти в точку j, то будет справедливо утверждение А_j. Для циклов точки i и j могут быть одной и той же точкой.

 Если справедливо А₁, то при прохождении по пути 1→2 будет справедливо А₂ и т.д.

Чтобы убедиться, что таким образом действительно доказывается частичная правильность, докажем теорему.

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

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

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

2. Предположим, что мы прошли n точек и попали в некоторую точку i_n, с которой связано утверждение . Предположим, что утверждение  справедливо (гипотеза индукции). Нужно доказать, что если выполнение программы продолжается, и мы из точки i_n попали в точку i_n+1, то при ее достижении будет справедливо утверждение . Справедливость этого факта для каждого пути, связывающего точки i_n и i_n+1, мы доказали в методе индуктивных утверждений (пункт 2). Таким образом, если программа написана по правилам структурного программирования и является простой, то для каждой точки i будет справедливо утверждение А_i, так как существует путь через каждый узел от начала к концу программы. Тогда, если будет достигнута конечная точка программы, то будет справедливо и утверждение С.

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

Пусть имеется следующая программа поиска максимального значения среди элементов х_i,j.

1-8 – это точки, в которых предположительно имеют место следующие утверждения:

· А₁ : х – массив чисел, состоящий из m строк и n столбцов,

(исходная предпосылка);

 

· А₂ : , кроме того

· А₃: , , при этом .

 

· А₈ : .

 

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

1) Путь 1→2: , и т.к. из , то , т.е. утверждение А₂ справедливо.

2) Путь 2→3: Дано утверждение А₂. Требуется доказать А₃. При первом вхождении в точку 3 ,следовательно, , т.к. . Из утверждения А₂, т.к. i не менялось, имеем , но в силу ограничения цикла в точке 2 в точке 3 получаем . Если , то из утверждения А₂ следует , иначе, когда , из утверждения А₂ получаем, что . Более того, можно утверждать, что , т.к. . Таким образом, видно, что при переходе из точки 2 в точку 3 утверждение А₃ оказывается справедливым.

3) Путь 3→4→5→3. Пусть справедливо утверждение А₃. Покажем, что оно остается справедливым при переходе по данному пути. Пусть в точке 3 в какой-то момент времени , для которых выполняются неравенства: , . Тогда при переходе по пути 3→4→5→3 получаем , где . Так как мы двигались по указанному выше пути, то проверка  в цикле была истинной, следовательно, . Значение  не менялось, кроме того, мы приходим в точку 3 с условием , следовательно,  остается максимальным и для нового значения j, т.е. утверждение А₃ остается справедливым.

4) Путь 3→4→6→3. Доказательство аналогично пункту 3 за исключением того, что здесь нашлось , и переменной  присвоено это значение. Таким образом, утверждение А₃ остается также справедливым.

5) Путь 3→7→2. Пусть справедливо утверждение А₃. Покажем, что при прохождении пути 3→7→2 будет справедливо утверждение А₂. Из точки 3 в точку 2 мы попадаем, когда ложна проверка , но из А₃ известно, что . Отсюда следует, что  или . Тогда утверждение A₃ относительно  перепишется в виде . Но при прохождении пути 3→7→2 , поэтому , . Утверждение А₂ справедливо.

6) Путь 2→8. Так как мы вышли из точки 2 в точку 8 проверка неравенства  оказалась ложной, следовательно,  и утверждение A₂ , что , преобразуется в утверждение A₈ о частичной правильности программы: .

⇐ Предыдущая3456789101112Следующая ⇒

Поделиться: