9.9. Доказательство свойств корректности

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

Аксиомы собственно модальной логики, часть из которых была рассмотрена в начале настоящей главы. Эти аксиомы, как обычно, назовем базовыми аксиомами.

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

Общие аксиомы, описывающие свойства модели параллельных процессов (программы), не зависящие от конкретного типа программы, свойства корректности которой необходимо доказать. Эти аксиомы, как обычно, назовем модельными аксиомами.

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

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

В настоящем параграфе ограничимся рассмотрением примера доказательства корректности для простой программы (рис. 9.7), содержащей только один процесс и, следовательно, являющейся последовательной детерминированной программой. Мы не будем выписывать все известные к настоящему времени базовые аксиомы и правила модальной логики. Будем вводить эти аксиомы и правила по мере необходимости в ходе доказательства.

9.9.1. Модельные аксиомы

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

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

9.9.2. Программные аксиомы

Рассмотрим программу возведения в целую степень действительного числа т.е. программу вычисления Эта программа имеет три места

Место является начальным и до начала вычисления истинно действие -1 Начать. Вычисление начинается в результате выполнения действия Начать.

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

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

(см. скан)

Рис. 9.7. Граф переходов программы возведения в целую степень числа

9.9.3. Свойство корректности

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

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

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

Для того чтобы было удобно следить за процессом доказательства корректности программы, каждый его шаг будем нумеровать. Как всегда, формула со знаком впереди означает, что она стала истинной в результате вывода на этом шаге. Выше будем указывать те правила или аксиомы, которые использовались для доказательства ее истинности. Некоторые из этих правил и аксиом ранее нигде не упоминались. Большинство из этих правил легко вывести из правил и аксиом, рассмотренных в предыдущих главах. Если потребуется, то будем давать также пояснения к доказательству на соответствующем шаге. В соответствии с приведенным ранее определением ситуация 5 есть состояние программы, когда она находится в месте и ожидает выполнения очередного действия для перехода в другую ситуацию (место при этом может оказаться тем же самым). Обратим внимание, что как только программа попадет в место I, переменным набора у присваиваются значения промежуточного набора и и вычисляется очередное промежуточное значение

Начальное условие имеет вид

Используя программную аксиому и подставляя вместо ее значение, равное 1, получаем

т.е. имеем истинную формулу

(кликните для просмотра скана)

Используя программную аксиому формулу (9.10) и правило модус поненс, получаем истинную формулу для случая, когда

Используя профаммную аксиому формулу (9.12) и правило модус поненс, получаем истинную формулу для случая, когда и нечетный

Используя программную аксиому формулу (9.13) и правило модус поненс, получаем истинную формулу для случая, когда и четный

Предположим теперь, что формула

истинна для любого места

Тогда используя программную аксиому формулу (9.14) и правило модус поненс, получаем истинную формулу для случая, когда четный

Используя профаммную аксиому формулу (9.15) и правило модус поненс, получаем истинную формулу для случая, когда и нечетный

Используя программную аксиому формулу (9.16) и правило модус поненс, получаем истинную формулу для случая, когда и четный

Других формул не существует. Таким образом, показана истинность и истинность Из индукционной аксиомы следует истинность формулы

Используя аксиому модальной логики получаем

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

Используя правило исключения конъюнкта, получаем месте

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

Корректность профаммы доказана.

Вопросы и упражнения

(см. скан)

(см. скан)