Логика Хоара

Аксиомы PDL

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

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

Шкала Крипке (или система переходов) будет состоять из пары: (W, R_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, h), состоящая из шкалы Крипке и оценки h: P®P(W), удовлетворяющих соотношениям:

1) R_aÈb=R_aÈR_b;

2) R_a;b=R_a°R_b;

3) R_p*=ÈR_pⁿ, nÎ{0,…,¥};

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

Здесь R_p* – наименьшее рефлексивное транзитивное отношение, содержащее R_p.

Расширим h на множество формул F(P), полагая wÎh(A), если и только если (M, w|-A). Получим соотношения:

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

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

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

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

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

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

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

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

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

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

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

6) AÚ<a><a*>A «<a*>A;

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

Аксиомы 1 – 2 стандартны для модальных логик. Аксиома 7 равносильна аксиоме Сегерберга [a*](A ® [a]A) ® (A ® [a*]A) и называется аксиомой PDL – индукции.

Правила вывода для данной теории:

1) Modus ponens

2) UG: А

[a]A.

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

Хоар	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, можно получить следующие правила вывода логики Хоара:

1) Композиция: {А}a{В},{В}b{С}

{А}a;b{С}

2) Условие: {A&B}a{C},{A&ØB}b{C}

{A} if B then a else b{C}

3) Цикл: {A&B}a{A}

{A} do B ® a od {A&ØB}

4) Следствие: A®A’,{A’}a{B’}, B’®B

{A}a{B}

[1] Что и требовалось доказать

[2] Напомним, что одним из признаков умозаключения является наличие в высказывании слова «следовательно».

[3] Напомним, что терм – это предметная переменная, или предметная постоянная, или функциональный символ с аргументами–термами.

[4] и.п. - исчисление предикатов

[5] и.в. – исчисление высказываний

[6] Раздел 6.1 - по материалам: А.А.Ивин «Логика», учеб. пособ., М.: изд-во «Знание», 1998

[7] Подобная интерпретация семантики операторов принята только в рамках данного пособия

[8] Читается как: формула А выполняется в мире w для модели М

[9] При этом под состоянием машины понимается содержимое оперативной памяти компьютера.

[10] Propositional Dinamic Logic

Дата добавления: 2014-01-04