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

Введем обозначение (триада Хоара)

{Q} S {R}, (2.2)

где Q, R - предикаты, S - программа (оператор или последовательность операторов). Обозначение определяет следующий смысл: «Если выполнение S началось в состоянии, удовлетворяющем Q, то имеется гарантия, что оно завершится через конечное время в состоянии, удовлетворяющем R».

Предикат Q называется предусловием или входным высказыванием S, предикат R - постусловием или выходным высказыванием. Следовательно, R определяет то, что нужно установить. Можно сказать, что R определяет спецификацию задачи. В предусловии Q нужно отражать тот факт, что входные переменные получили начальные значения.

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

Пример 2.3. Рассмотрим оператор присваивания для целочисленных переменных и постусловие:

sum := 2 * х + 1 {sum > 1}

Одним из возможных предусловий данного оператора может быть {х > 10}.

Слабейшими предусловиями называются наименьшие предусловия, обеспечивающие выполнение соответствующего постусловия. Например, для приведенного выше оператора и его постусловия предусловия {х > 10}, {х > 50} и {х > 1000} являются правильными. Слабейшим из всех предусловий в данном случае будет {х > 0}.

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

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

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

Если 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).

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

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