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

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

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

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

Рис. 3.1.

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

1) {А₁  С} S1{А₂}

и

2) {А₁   С} S2{А₂},

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

3) {А₁} IF С ТНЕN S1 ЕLSЕ S2 {А₂}.

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

1'. Если мы попали в точку 1 и справедливо утверждение А₁ а затем проходим от точки 1 через точку 3 до точки 2, то А₂ справедливо. Но для этого же пути известно, что до выполнения 51 справедливы и утверждение А₁ и условие С, и мы стремимся показать, что если попадем в точку 2 (т.е. если выполнение S1 закончится), то А₂ будет справедливо.

2'. Если мы попадем в точку 1 и справедливо утверждение А₁ а затем проходим от точки 1 через точку 4 до точки 2, то А₂ справедливо. Но для этого пути известно, что до выполнения S2 справедливо А₁ и ложно условие С (т.е.  С справедливо). Мы стремимся показать, что если попадем в точку 2 (т.е. при условии окончания S2), то будет справедливо А₂.

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