Пропозициональная динамическая логика

Алгоритмическая логика

Since, Until

Для любых формул А и В добавляются формулы ASB и AUB. Семантика в моде-

ли M=(W, <, h):

· (M, w|-AUB), если и только если для некоторого w₁>w верно (M, w₁|-B) и при всех v, удовлетворяющих соотношениям w<v<w₁, верно (M, v|-A), т.е. А верно до тех пор, пока не В;

· (M, w|- ASB), если и только если для некоторого w₁<w верно (M, w₁|-B), а для всех v, удовлетворяющих соотношениям w₁<v<w, верно (M, v|- A), т.е. с тех пор, как случилось В, верно А.

В 70-х годах XX века назрела проблема верификации программных комплексов. Необходимо было так описать семантику языка программирования, чтобы писать программу вместе с доказательством ее верности, а для этого необходимо построить логическую систему, опирающуюся на аксиоматику и правила вывода каждой конструктивной единицы языка программирования. Так начала формироваться алгоритмическая логика.

Интуитивно программа понимается как набор операторов, переводящих машину из одних состояний в другие. Хоар предложил для отладки и верификации программ рассматривать формулы, описывающие состояния машины перед выполнением (предусловие) и после выполнения (постусловие) программы. Программе p сопоставлялась запись: {А}p{В}, означающая, что предусловие описывается формулой А, а постусловие - формулой В. Пратт предложил запись: А ® [p]В – если перед выполнением программы состояние машины описывается формулой А, то после выполнения верна формула В. Это позволило описывать вычислительные процессы, состоящие из комплексов программ, с помощью модальной логики, рассматривая каждую программу как модальность.

Пусть P₀ – произвольное множество, элементы которого называются базисными программами. Предположим, что PÊP₀ – такое множество слов, что вместе с любыми p₁, p₂ÎP оно содержит:

1) p₁Èp₂ (неопределённый выбор одной из программ p₁ или p₂);

2) p₁;p₂ (выполнение p₁, затем p₂);

3) p₁* (выполнение p₁ конечное, возможно нулевое, количество раз);

4) p₁Çp₂ (одновременное выполнение программ p₁ и p₂).

Элементы из P будем называть программами. Рассмотрим атомы из Р как простые высказывания о состояниях машины, в которую загружаются программы[9]. Для каждой программы pÎP обозначим через [p] соответствующую ей модальность. Определим формулы пропозициональной динамической логики PDL[10] по индукции:

1) атомы рÎР – формулы;

2) А&В, ØА, [p]А – формулы для любых формул А, В и элемента pÎP;

3) все формулы PDL составляются с помощью правил 1 – 2.

Введём обозначение: <p>А как сокращение для Ø[p]ØА.

Для каждой формулы А определим программу: А?ÎP, тестирующую, верна ли формула А. Эта программа заканчивает работу, если формула А верна, и зависает (аварийно завершает работу) в противном случае. Эта программа вводится с целью интерпретации оператора if (A) then p₁ else p₂ как программы (А?; p₁)È((ØА)?; p₂)ÎP.