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

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

Since, Until

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

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

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

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

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

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

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

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

2) p1;p2 (выполнение p1, затем p2);

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

4) p1Çp2 (одновременное выполнение программ p1 и p2).

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

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

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

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

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

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