Преобразователь предикатов
Введем обозначение (триада Хоара)
{ 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).
Если для каждого оператора языка по заданным постусловиям можно вычислить слабейшее предусловие, то для программ на данном языке может быть построено корректное доказательство. Доказательство начинается с использования результатов, которые надо получить при выполнении программы, в качестве постусловия последнего оператора программы, и выполняется с помощью отслеживания программы от конца к началу с последовательным вычислением слабейших предусловий для каждого оператора. При достижении начала программы первое ее предусловие отражает условия, при которых программа вычислит требуемые результаты.
|
|
Для некоторых операторов программы вычисление слабейшего предусловия на основе оператора и его постусловия является достаточно простым и может быть задано с помощью аксиомы. Однако, как правило, слабейшее предусловие вычисляется только с помощью правила логического вывода, т.е. метода выведения истинности одного высказывания на основе значений остальных высказываний.
Дата добавления: 2015-12-20; просмотров: 31; Мы поможем в написании вашей работы! |
Мы поможем в написании ваших работ!