 B2  s2 Si – оператор или их последовательность

. . .

 B_n  SN

fi

• На порядок проверки предохранителей не накладывается ограничений: если несколько из них истинны, то недетерминизм

• Если некоторый B_i не определен или ни один из них не истина, то программа прекращается (аварийный останов - авост)

Основная теорема для IF

Пусть предикат Q таков, что:

1. Q  B₁  B₂  ...  B_n

2. Q & B_i  wp ( Si, R ) ( 1  i  n )

Тогда и только тогда Q  wp ( IF, R)

Используя три описанных оператора, можно синтезировать простейшую программу одновременно с доказательством ее правильности. Пример: для фиксированных x, y найти максимальный их них. Формальная спф задачи:

{ T } S { R: z = max (x, y) };

логическое определение функции max: R: (z = x  z = y) & z  x & z  y

Какую команду выполнить, чтобы получилось R ? Попробуем z := x. Когда она должна выполниться ?

Wp( ‘z:=x’, R ) =

= ( x = x  x = y) & x  x & x  y =

= ( T  x = y) & T & x  y =

= x  y

Следовательно, B₁ – это x  y и эскиз программы: if x  y  z := x fi

Чтобы не было авоста, нужен как минимум еще один предохранитель. Из теоремы: Q  B₁  B₂. Другая возможность получить R - выполнить x := y. Рассуждая аналогично, получим: В₂ это y  x .

В результате: if x  y  z := x

 y  x  z := y

fi

Поскольку ( x  y  y  x) = T (тождественно истина), то авоста не будет.

При x = y программа недетерминированная.

4. Оператор цикла while B do S: его семантика описывается с помощью инварианта цикла – предиката, истинного перед входом в цикл и после каждого выполнения тела цикла, в том числе в момент его завершения. Завершаемость, т.е. конечное число повторений цикла, описывается отдельным условием – целочисленной ограничивающей функцией.

В упрощенном виде основная теорема для цикла:

Если P & B wp (S, P), то P  wp (while B do S, P &  B) (если цикл завершается).

Пример инварианта - для цикла суммирования массива из 10 элементов b[i]

i:= 1; S:= b[0];

{ P }

while i < 10 do S:= S + b[i]; i:= i + 1 od { P };

{R : S =  (k=0, 9) b[k] }

Инвариант P : 1  i 10 & S =  (k=0, i-1) b[k]

т.е., на i-ом повторении цикла S - частичная сумма первых i элементов массива.

То, что неформально понимается программистом, здесь получает строго формальное выражение. Рекомендуется инвариант цикла строить до построения самого цикла.

(Задание 3).

Трудности и ограничения метода:

• Доказательство громоздко – длиннее самой программы – и может содержать ошибки

• Семантику машинных операций (вв/вы, вызов подпрограмм) трудно описать на языке предикатов 1-го порядка

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

Литература

1. Д. Грис. Наука программирования. М, Наука, 1985.