Интуитивно программа понимается как набор операторов, переводящих машину из одних состояний в другие. Хоар предложил для отладки и верификации программ рассматривать формулы, описывающие состояния машины перед выполнением (предусловие) и после выполнения (постусловие) программы. Программе 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 будем называть программами. Рассмотрим атомы из Р как простые высказывания о состояниях машины, в которую загружаются программы. Для каждой программы p Î P обозначим через [p] соответствующую ей модальность. Определим формулы пропозициональной динамической логики PDL по индукции:

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

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

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

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

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

if (A)  then  p₁  else  p₂

как программы

(А?; p₁) È ((ØА)? ; p₂) Î P.

Семантика пропозициональной динамической логики

Пусть P₀ – множество базисных программ, P – множество всех программ, Р – атомные формулы, F(P) – все формулы, W – множество состояний машины, в которой могут работать программы pÎP. Для каждого p Î P определена модальность [p]. Стало быть, мы должны каждому p поставить в соответствие некоторое отношение доступности R_p Í W ´ W.

Шкала Крипке (или система переходов) будет состоять из пары: (W, (R_p)_pÎP), где W – множество состояний, а R_{p –} отношения R_p Í W ´ W.

Программу можно интерпретировать как множество пар (x, y) Î R_p таких, что после выполнения программы p машина из состояния х перейдёт в состояние y. Каждому атому p Î P ставится в соответствие подмножество h(p) Í W состояний, при которых высказывание р верно.

Интерпретацией называется тройка M = (W, (R_p)_pÎP, h), состоящая из шкалы Крипке и оценки h : P ® P(W), удовлетворяющих соотношениям:

1) R_a È _b = R_a È R_b;

2) R_a ; _b = R_a ° R_b;

3) ;

4) R_A? = {(x, x) : x Î W и M, x |= A}.

Здесь R_p* – наименьшее рефлексивное транзитивное отношение, содержащее R_p. Расширим h на множество формул F(P), полагая t Î h(A), если и только если M, t |= A. Получим соотношения:

5) h(A Ú B) = h(A) Ú h(B);

6) h(ØA) = W h(A);

7) h(<p>A) = {t Î W : (t, u) Î R_p  для некоторого u Î h(A)}.

В некоторых случаях под семантикой логики PDL понимают шкалу с расширенной на F(P) оценкой, удовлетворяющие соотношениям 1 – 7.

Аксиомы PDL

Можно ожидать, что для любых формулы А и программы p Î P формула <p*>А, (означающая возможность того, что после кратного применения p машина перейдёт в состояние, удовлетворяющее формуле А), будет равносильна формуле А Ú <p; p*>А, (означающей, что верно А, или А будет, возможно, верно после применения p не менее, чем 1 раз). Получим аксиому:

<p*>А « А Ú <p; p*> А.

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

1) все тавтологии исчисления высказываний;

2) <a>A & <a>B « <a>(A & B);

3) <a>(A Ú B) « <a>A Ú <a>B);

4) <a Ú b>A « <a>A Ú <b>A;

5) <a ; b>A « <a><b>A;

6) <A?>B « A&B;

7) A È <a><a*>A « <a*>A;

8) <a*>A ® A Ú <a*> (ØA & <a>A).

Аксиомы 1 – 3 стандартны для модальных логик. Аксиома 8 равносильна аксиоме Сегерберга:

[a*](A ® [a]A) ® (A ® [a*]A)

и называется аксиомой PDL – индукции.

Правила вывода

;          .

Для формальной теории PDL справедливы теорема корректности и полноты.

Логика Хоара

Как мы уже отмечали, логика Хоара предназначалась для дедуктивного доказательства правильности программ. Её формулами являются тройки {А}p{В}, состоящие из предусловия А, программы p и постусловия В. Приведём форму записи, применяемой Хоаром, и её перевод на язык исчисления PDL:

skip	= 1?
fail	= 0?
if  A  then  a  else  b	= (A? ; a) È (ØA? ; b)
if  A1 ®  p1 |…| An  ®  pn fi	= (A1? ; p1) È … È (An? ; pn)
do  A ®  p  od	= (A? ; p)* ; (ØA)?
{A}p{B}	= A ® [p] B

Форма {A}p{B} называется тройкой Хоара. Логика Хоара является формальной теорией для вывода с помощью троек Хоара. Преобразуя аксиомы языка PDL, можно получить следующие правила вывода логики Хоара:

  (композиция)

  (условие)

  (цикл)

  (следствие).