Преобразователь предикатов

Э. Дейкстра рассматривает слабейшие предусловия, т.е. предусловия, необходимые и достаточные для гарантии желаемого результата.

«Условие, характеризующее множество всех начальных состояний, при которых запуск обязательно приведет к событию правильного завершения, причем система (машина, конструкция) останется в конечном состоянии, удовлетворяющем заданному постусловию, называется слабейшим предусловием, соответствующим этому постусловию».

Условие называют слабейшим, так как чем слабее условие, тем больше состояний удовлетворяют ему. Наша цель - охарактеризовать все возможные начальные состояния, которые приведут к желаемому конечному состоянию.

Если S - некоторый оператор (последовательность операторов), R - желаемое постусловие, то соответствующее слабейшее предусловие будем обозначать wp(S, R).

Аббревиатура wp определяется начальными буквами английских слов weakest (слабейший) и precondition (предусловие). Предполагается, что известно, как работает оператор S (известна семантика S), если можно вывести для любого постусловия R соответствующее слабейшее предусловие wp(S, R).

Определение семантики оператора дается в виде правила, описывающего, как для любого заданного постусловия R можно вывести соответствующее слабейшее предусловие wp(S, R).

Для фиксированного оператора S такое правило, которое по заданному предикату R вырабатывает предикат wp(S,R), называется «преобразователем предикатов»: {wp(S, R)} S {R}.

Это значит, что описание семантики оператора S представимо с помощью преобразователя предикатов. Применительно к конкретным S и R часто бывает неважным точный вид wp(S,R), бывает достаточно более сильного условия Q, т.е. условия, для которого можно доказать, что утверждение Q => wp(S, R) справедливо для всех состояний. Значит, множество состояний, для которых Q - истина, является подмножеством того множества состояний, для которых wp(S, R) - истина. Возможность работать с предусловиями Q, не являющимися слабейшими, полезна, поскольку выводить wp(S, R) явно не всегда практично.

Сформулируем свойства (по Э. Дейкстра) wp(S, R).

Свойство 1. wp (S, F) = F для любого S. (Закон исключенного чуда).

Свойство 2. Закон монотонности. Для любого S и предикатов P и R таких, что P => R для всех состояний, справедливо для всех состояний wp(S, P) => wp(S, R).

Свойство 3. Дистрибутивность конъюнкции. Для любых S, P, R справедливо

wp(S, P) AND wp(S, R) = wp(S, P AND R).

Свойство 4. Дистрибутивность дизъюнкции. Для любых S, P, R справедливо

wp(S, P) OR wp(S, R) = wp(S, P OR R).

Если для каждого оператора языка по заданным постусловиям можно вычислить слабейшее предусловие, то для программ на данном языке может быть построено корректное доказательство. Доказательство начинается с использования результатов, которые надо получить при выполнении программы, в качестве постусловия последнего оператора программы, и выполняется с помощью отслеживания программы от конца к началу с последовательным вычислением слабейших предусловий для каждого оператора. При достижении начала программы первое ее предусловие отражает условия, при которых программа вычислит требуемые результаты.

Для некоторых операторов программы вычисление слабейшего предусловия на основе оператора и его постусловия является достаточно простым и может быть задано с помощью аксиомы. Однако, как правило, слабейшее предусловие вычисляется только с помощью правила логического вывода, т.е. метода выведения истинности одного утверждения на основе значений остальных утверждений.

2.1.2.2. Аксиоматическое определение операторов языка программирования в терминах wp.

Определим слабейшее предусловие для основных операторов: оператора присваивания, составного оператора, оператора выбора и оператора цикла.

Оператор присваивания имеет вид: x:= E, где x - простая переменная, E – выражение (типы x и E совпадают).

Определим слабейшее предусловие оператора присваивания как Q = wp(x:= E, R), где Q получается из R заменой каждого вхождения x на E, что обозначим Q = R^x_Е.

Предполагается, что значение Е определено и вычисление выражения Е не может изменить значения ни одной переменной. Последнее ограничение запрещает функции с побочным эффектом. Следовательно, можно использовать обычные свойства выражений такие, как ассоциативность, коммутативность и логические законы.

Составной оператор имеет вид: begin S₁; S₂;...; S_n end

Определим слабейшее предусловие для последовательности двух операторов:

wp(S₁;S₂, R) = wp(S₁, wp(S₂, R)).

Аналогично слабейшее предусловие определяется для последовательности из n операторов.

Оператор выбора определим так: if B₁ → S₁ П B₂ → S₂ ... П B_n → S_n fi

Здесь n ³ 0, B₁, B₂,..., B_n - логические выражения, называемые охранами, S₁, S₂,..., S_n - операторы, пара B_i → S_i называется охраняемой командой, П - разделитель, if и fi играют роль операторных скобок.

Выполняется оператор следующим образом.

Проверяются все B_i. Если одна из охран не определена, то происходит аварийное завершение. Далее, по крайней мере, одна из охран должна иметь значение истина, иначе выполнение завершается аварийно.

Выбирается одна из охраняемых команд B_i → S_i, у которой значение B_i истина, и выполняется S_i.

Определим слабейшее предусловие:

wp(if, R) = BB AND (B₁ => wp(S₁, R)) AND... AND (B_n => wp(S_n, R)),

где BB = B₁ OR B₂ OR... OR B_n.

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

Естественно определить wp(if, R) с помощью кванторов:

wp(if, R) = ($ i: 1 £ i £ n: Bi) AND (" i: 1 £ i £ n: Bi => wp(Si, R))

Пример 2.4. Определить z = |x|.

С использованием оператора выбора: if x ³ 0 → z:= x П x £ 0 → z:= -x fi.

К особенностям оператора выбора следует отнести, во-первых, тот факт, что он включает условный оператор (if... then..), альтернативный оператор (if… then... else...) и оператор выбора (case).

Во-вторых, оператор выбора не допускает умолчаний, что помогает при разработке сложных программ, так как каждая альтернатива представлена подробно, и возможность что-либо упустить уменьшается.

В-третьих, благодаря отсутствию умолчаний, запись оператора выбора представлена в симметричном виде.

Оператор цикла. В обозначениях Э. Дейкстры цикл имеет вид: do B → S do.

Обозначим это соотношение через DO и представим его в следующем виде:

DO: do B₁ → S₁ П B₂ → S₂ ... П B_n → S_n od, где n ³ 0, B_i → S_i - охраняемые команды.

Выполняется оператор следующим образом. Пока возможно выбирается охрана B_i со значением истина, и выполняется соответствующий оператор S_i. Как только все охраны будут иметь значение ложь, выполнение DO завершится.

Выбор охраны со значением истина и выполнение соответствующего оператора называется выполнением шага цикла. Если истинными являются несколько охран, то выбирается любая из них.

Следовательно, оператор DO эквивалентен оператору

do BB → if B2 → S1 П B2 → S2... П Bn → Sn fi od или do BB → IF od,

где BB - дизъюнкция охран, IF - оператор выбора.

Пример 2.5. Алгоритм Евклида.

Вариант 1.

задать (N, M);

if N > 0 AND M > 0 →n, m:= N, M;

do n ≠ m → if n > m → n:= n – m П m > n → m:= m – n fi od;

выдать (n)

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