ТЕОРИЯ ВЫЧИСЛИТЕЛЬНЫХ СИСТЕМ. Теория вычислительных процессов
 Скачать 2.17 Mb.
|
|
Аксиоматическая семантика Аксиоматическая семантика была создана в процессе разработки метода доказательства правильности программ. Данный метод распространяет на программы область применения исчисления предикатов. Семантику каждой синтаксической конструкции языка можно определить как некий набор аксиом или правил вывода, который можно использовать для вывода результатов выполнения этой конструкции. Чтобы понять смысл всей программы (то есть разобраться, что и как она делает), эти аксиомы и правила вывода следует использовать так же, как при доказательстве обычных математических теорем. В предположении, что значения входных переменных удовлетворяют некоторым ограничениям, аксиомы и правила вывода могут быть использованы для получения (вывода) ограничений на значения других переменных после выполнения каждого оператора программы. В конце концов, когда программа выполнена, мы получаем доказательство того, что вычисленные результаты удовлетворяют необходимым ограничениям на их значения относительно входных значений. То есть, доказано, что выходные данные представляют значения соответствующей функции, вычисленной по значениям входных данных. Такие доказательства показывают, что программа выполняет вычисления, описанные ее спецификацией. В доказательстве каждый оператор программы сопровождается предшествующим и последующим логическими выражениями, устанавливающими ограничения на переменные в программе. Эти выражения используются для определения смысла оператора вместо полного описания состояния абстрактной машины (как в операционной семантике). 2.1.2.1. Краткое введение в исчисление высказываний Аксиоматическая семантика основана на математической логике. Будем называть предикат, помещенный в программу высказыванием (иногда употребляют термин утверждение). Высказывание, непосредственно предшествующее оператору программы, описывает ограничения, наложенные на переменные в данном месте программы. Высказывание, следующее непосредственно за оператором программы, описывает новые ограничения на те же (а возможно, и другие) переменные после выполнения оператора. Обычно термин высказывание используется для логических переменных, принимающих одно из двух значений F и Т, которые представляют понятия «ложь» и «истина». На значениях типа «логический» определены пять операций: отрицание: (NOT b), конъюнкция: (b AND с), дизъюнкция: (b OR с), импликация: (b  с), равенство: (b = с). Высказывания строятся по следующим правилам.1.F и Т – высказывания. 2.Идентификаторы (непустая последовательность букв и цифр, начинающаяся с буквы) являются высказываниями. 3.Если b – высказывание, то (NOTb) высказывание. 4.Если b и с – высказывания, то (b OR с), (b AND с), (b = с), (b с) – также высказывания. Вычисление постоянных высказываний, содержащих в качестве операндов только константы, имеет три определяемых структурой высказывания E случая: E без операций, E с одной операцией, E с более чем одной операцией. 1.Значение Т есть Т, значение F есть F. 2.Значения (NOT b), (b AND с), (b OR с), (b с), (b = с), где b и с – константы F и Т в любой комбинации, определяются по таблице, называемой таблицей истинности.
3.Значение постоянного высказывания, содержащего более чем одну операцию, получается последовательным применением таблицы истинности к подвысказываниям этого высказывания и заменой подвысказываний на их значения до тех пор, пока высказывание не сведется к F или Т. Состояние s – это функция из множества идентификаторов в множество значений F и Т. ВысказываниеEопределено в состоянииs, если каждый идентификатор из E встречается в s. s(E) – значение E в состоянии s – получаемое заменой всех вхождений идентификаторов b в высказывание E на их значения s(b) и вычислением получившегося постоянного высказывания. Тавтология – высказывание, истинное в любом состоянии, в котором оно определено. Высказывание выражает, или описывает, множество состояний, в котором оно истинно. Правила старшинства операций: 1.Последовательность одноименных операций вычисляется слева направо. 2.Порядок вычислений различных между собой и смежных в записи высказывания операций определяется списком: NOT, AND, OR, , =. Вычисление высказываний редко бывает самоцелью. Чаще необходимо манипулировать ими, чтобы вывести «эквивалентные», но более простые высказывания. Высказывания Е1 и Е2 эквивалентны, если и только если Е1 = Е2 есть тавтология. Здесь Е1 Е2 эквивалентность. 1. Законы коммутативности: (Е1  Е2) = (Е2 Е1), - обозначает операции = , AND, OR.2. Законы ассоциативности: (Е1 Е2) Е3 = Е1 (Е2 Е3), - обозначает операции AND, OR.3. Законы дистрибутивности: (Е1 Е2) Е3 = (Е1 Е3) (Е2 Е3), и - обозначают операции AND, OR.4. Законы де Моргана: NOT (Е1 Е2) = NOT Е1 NOT Е1), и - обозначают операции AND, OR.5. Закон отрицания: NOT (NOT Е1) = Е1. 6. Закон исключенного третьего: Е1 OR NOT Е1 = Т. 7. Закон противоречия: Е1 AND NOT Е1 = F. 8. Закон импликации: : (Е1 Е2) = NOT Е1 OR Е2.9. Закон равенства: (Е1 = Е2) = (Е1 Е2) AND (Е2 Е1).10.Законы упрощенияOR: Е1 OR Е1 = Е1, Е1 OR (Е1 AND Е2) = Е1,Е1 OR Т = Т, Е1 OR F = Е1. 11.Законы упрощенияAND: Е1 AND Е1 = Е1, Е1 AND (Е1 OR Е2) = Е1,Е1 AND Т = Е1, Е1 AND F = F. 12.Закон тождества Е1 = Е1. Для вычисления высказываний используют правила подстановки и транзитивности. Правило постановки: Если е1 = е2 – эквивалентность, а Е(х) – высказывание, записанное как функция от одного из своих идентификаторов х. Тогда Е(е1) = Е(е2) и Е(е2) = Е(е1) эквивалентности. Правило транзитивности: Если е1 = е2 и е2 = е3 – эквивалентности, то е1 = е3 - эквивалентности. Для формулирования развернутых высказываний используются кванторы. Квантор существования (i: m  i < n: Ei). Квантор всеобщности (i: m i < n: Ei) = NOT (i: m i < n: NOT Ei)Множество значений, удовлетворяющих m i < n, называется областью значений квантифицированной переменной i.Вхождение идентификатораiв предикат называется связанным, если оно находится в области действия квантора i или i, и свободным в противном случае. В одном и том же выражении один и тот же идентификатор не может быть как связанным, так и свободным и идентификатор не может быть связан двумя различными кванторами. 2.1.2.2. Преобразователь предикатов Введем обозначение (триада Хоара) {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). Если для каждого оператора языка по заданным постусловиям можно вычислить слабейшее предусловие, то для программ на данном языке может быть построено корректное доказательство. Доказательство начинается с использования результатов, которые надо получить при выполнении программы, в качестве постусловия последнего оператора программы, и выполняется с помощью отслеживания программы от конца к началу с последовательным вычислением слабейших предусловий для каждого оператора. При достижении начала программы первое ее предусловие отражает условия, при которых программа вычислит требуемые результаты. Для некоторых операторов программы вычисление слабейшего предусловия на основе оператора и его постусловия является достаточно простым и может быть задано с помощью аксиомы. Однако, как правило, слабейшее предусловие вычисляется только с помощью правила логического вывода, т.е. метода выведения истинности одного высказывания на основе значений остальных высказываний. 2.1.2.3. Аксиоматическое определение операторов языка программирования в терминах wp. Определим слабейшее предусловие для основных операторов: оператора присваивания, составного оператора, оператора выбора и оператора цикла. Оператор присваивания имеет вид: x := E, где x - простая переменная, E – выражение (типы x и E совпадают). Определим слабейшее предусловие оператора присваивания как Q = wp(x := E, R), где Q получается из R заменой каждого вхождения x наE, что обозначим Q = RxЕ. Предполагается, что значение Е определено и вычисление выражения Е не может изменить значения ни одной переменной. Последнее ограничение запрещает функции с побочным эффектом. Следовательно, можно использовать обычные свойства выражений такие, как ассоциативность, коммутативность и логические законы. Составной оператор имеет вид: begin S1; S2; ... ; Sn end Определим слабейшее предусловие для последовательности двух операторов: wp(S1;S2, R) = wp(S1, wp(S2, R)). Аналогично слабейшее предусловие определяется для последовательности из n операторов. Оператор выбора определим так: if B1 → S1 П B2 → S2 ... П Bn → Sn fi Здесь n 0, B1, B2, ..., Bn - логические выражения, называемые охранами, S1, S2, ..., Sn - операторы, пара Bi → Si называется охраняемой командой, П - разделитель, if и fi играют роль операторных скобок. Выполняется оператор следующим образом. Проверяются все Bi. Если одна из охран не определена, то происходит аварийное завершение. Далее, по крайней мере, одна из охран должна иметь значение истина, иначе выполнение завершается аварийно. Выбирается одна из охраняемых команд Bi → Si, у которой значение Biистина, и выполняется Si. Определим слабейшее предусловие: wp(if, R) = BB AND (B1 => wp(S1, R)) AND ... AND (Bn => wp(Sn, R)), где BB = B1 OR B2 OR ... OR Bn. Предполагается, что охраны являются всюду определенными функциями (значение их определено во всех состояниях). Естественно определить 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 od. Обозначим это соотношение через DO и представим его в следующем виде: |