Р.У. Себеста - Основные копцепции языков программирования (2001) (1160794), страница 42
Текст из файла (страница 42)
А вот как: данный оператор присваивания с предусловием и постусловнем может рассматриваться как теорема; теорема считается доказанной, если аксиома присваивания, применяемая к постусловию и оператору присваивания, дает заданное предусловие. Рассмотрим, логическое утверждение (х > 3) х х - 3 (х > О) Глава 3. Описание синтаксиса и семантики Применение аксиомы присваивания к постусловию и оператору х и — 3 (х>01 дает ( х > 31, что и является заданным предусловием. Следовательно, предыдущее логическое утверждение доказано. Далее, рассмотрим логическое выражение (х > 5) х = х - 3 (х > О] В этом случае заданное предусловие ( х > 51 не соответствует утверждению, порождаемому применением аксиомы. Несмотря на это, очевилно, что (к > 5) => (х > 3).
Для использования этого фалта в доказательстве нам необходимо правило логического вывода, называемое правилом логического следствия (ги1е от сопзеооепсе). Общая форма правила логического вывода следующая: 51,52,...,5п 5 В ней утверждается, что из истинности выражений 51, 52, ... и 5п может быть выведена истинность утверждения 5. Правило логического следствия имеет форму (Р)5(а Р = Р()= О (Р')5(а Символ "=>" означает "следует", а 5 может быть любым оператором программы.
Правило формируется следующим образом: если истинно логическое утверждение (Р)5(О), то из утверждения Р' следует утверждение Р, а из утверждения О' следует утверждение (3, тогда можно доказать, что (Р')5Я'). Проще говоря, правило логического слелствия утверждает, что постусловие всегда может быть ослаблено, а предусловие— усилено. В доказательстве программы этот факт довольно полезен, поскольку он позволяет, например, завершить доказательство последнего из приведенных выше логических выражений.
Если мы будем считать, что в нашем случае Р— это (х >3), О н О' — (х > О), а Р' — (х > 5), то мы получим (х >3)х = х-3(х >0),(х >5) =>(х >3) (х >О) =>(х >О) (х > 5)х = х -3(х > О) Доказательство завершено. 3.6.2.4. Последовотельностн Слабейшее предусловие последовательности операторов невозможно описать с по. мощью аксиомы, поскольку предусловие зависит от конкретного вида операторов в последовательности. В этом случае единственной возможностью описания прелусловий является использование правила логического вывода.
Пусть 51 и 52 — соселние операторы программы. При следующих предусловиях и постусловиях этих операторов (Р1) 51 (Р2) (Р2) 52 (РЗ) правило логического вывода подобной двухоператорной последовательности будет таким: З.б. Описание смысла программ: динамическая семантика (РЦБЦ Р2). (Р2)$2(РЗ) (РЦЯ;$2(РЗ) Итак. лля приведенного выше примера выражение (Р1)$1гб2(РЗ) описывает аксиома~ пчссклю семантику последовательности операторов 51;$2. Если операторы Б) и 82 являются операторами присваивания х) = Е) х2 = Е2, г ~ имеем (РЗ е ) х2 = Е2 (РЗ) ((РЗ.,г.)„а) х! = Е1 (РЗ„, е.). Следовательно, слабейшим прелусловиелг последовательности х) = Е1; х2 =Е2 с пол тусловием РЗ является ((РЗх2-чЕ2)х1-+Е1). Рассмотрим последовательность операторов и постусловие: 3'х+1; х !х < 10! Прелусловием послелнего оператора присваивания является у с / Оно же становится постусловием лля первого оператора. Теперь мы можем вычисгпп ь прелусловие первого оператора присваивания: 3 х ч ' < 7 х 2 3.6.2.5.
Выбор Дачее мы рассмотрим правило логического вывода для операторов ветвления. Мы бл лсм поучать только операторы ветвления, содержащие оператор е1ае. Правило логическа~ о вывода для таких выражений записывается следующим образом: (В апг( Р) Б! (О), ((по! В) апг) Р) Е2 (( г) (Р) Ю В т(зеп $1 е!яе 52 ((3) 'Зто правило указывает, что ланные операторы ветвления лолжны быть доказаны для обоих случаев. Первое из написанных над чертой логических выражений относится к оператору С)чвп.
второе — к оператору е1ве. 1'ассмотрим пример вычисления с использованием правила логического вывола лля о~гсра горов ветвления. Возьмем следующий оператор ветвления: хЕ!х >О) -1 в1аву у + 1 Предположим, что постусловием для этого оператора выбора является (у > О). В с.
гучас выбора оператора аЬеп мы можем использовать аксиому присваивания: —. у-1(у>0! Глава 3. Описание синтаксиса и семантики 156 Это даетусловие (у — 1 > б) или (у >,'. Применим туже аксиому к варианту е1ее: у-у+1(у>б) Это порождает предусловие ! у 1 > О) или (у > -1). Поскольку (у >- 1) => (у > -1), то правило логического следствия разрешает нам использовать в качестве предусловия оператора выбора условие (у > ' ).
Э.б.2.б. Логмчвскм управляемый цикл с предварительной лроверкой условия Другой необходимой конструкцией императивных языков программирования является цикл с прелварительной проверкой условия, или цикл ип11е. Вычисление слабейшего предусловия для такого цикла изначально предполагается более сложным. чем для последовательности операторов. поскольку в общем случае число повторений цикла определить заранее невозможно.
Если число повторений цикла известно. то такой цикл можно трактовать как последовательность операторов. Проблема вычисления слабейшего предусловия для циклов подобна проблеме доказательства теоремы обо всех натуральных числах. В последнем случае обычно используется индукция, тот же метод мы используем и для циклов. Основным шагом индукции является определение индуктивного предположения. Соответствующим шагом в аксноматической семантике для цикла иЬ11е является поиск утверждения, называемого инвариантом мнила ()оор )птаг)апг), что является ключевым этапом обнаружения слабейшего предусловия. Правило логического вывода для вычисления предусловия цикза ип11е выглядит следующим образом: (1 апб В) Б(1) (Ц зтЬ(1е В до 8 епд (1апг) (пог В)) гле 1 — инвариант цикла.
Аксиоматическое описание цикла иЬ11е записывается следующим образом: (Р) ип11е В с(о Б епс1 Я) Инвариант цикла должен удовлетворять большому количеству условий. Во-первых. из слабейшего предусловия цикла и)з11е должна следовать истинность инварианта цикла. Во-вторых, из истинности инварианта цикла должна следовать истинность постусловия после завершения цикла.
Эти ограничения приводят нас от правила логического вывода к аксиоматическому описанию. Во время выполнения цикла результаты вычисления булевского выражения, управляющего циклом, и операторы тела цикла не должны влиять на истинность инварианта цикла. Поэтому он и называется инвариантом. Еше одним усложняющим фактором для циклов иЬ11в является вопрос о завершении цикла. Если () — постусловне, выполняющееся непосредственно после выхода нз цикла, то предусловие цикла Р обеспечивает истинность условия () на момент выхода из цикла, а также собственно завершение цикла.
Полное аксиоматнческое описание цикла и)з11е требует истинности всех следующих условий (через 1 обозначен инвариант цикла): 3.6. Описание смысла программ: динамическая семантика Р => ! (!) В(ц (! ало' В) 5 (!) (! апо'(по(В)) => О. завершение цикла Чтобы найти инвариант цикла, используем метод. подобный методу определения ниц) ктивного предположения математической индукции. Для нескольких случаев вычисляются зависимости в належде найти общую закономерность. При таком подходе удобно рассматривать процесс создания слабейшего предусловия как функцию тгр. В общем слкчае: жр (оператор, постусловие) = предусловие Для того чтобы обнаружить инвариант цикла (, используем постусловие цикла О для вычисления предусловий нескольких повторений тела цикла, начав с нуля повторений. Если тело цикла солержит один оператор присваивания, то для операторов присваивания используется аксиома.
Рассмотрим пример цикла ипа1в у <> х ао у = у + ! впс( (у х) Будьте осторожны и помните, что знак равенства в данном случае имеет два различных смысла. В утверждениях он означает математическое равенство; вне их он является оператором присваивания. Для нулевого количества повторений цикла значение слабейшего предусловия очевидно: (у = х) Для одного повторения; нР(у = у+ 1, (у = х)) (у+ 1 = х), или (у х — 1) Для двух нР(у = у + 1 (у" х -1)] = (у + 1 = х -1), или (у = х - 2) Для трех повторений нР(У = У + 1~ (У = х -2)) = (у + 1 х -2), или (у х - 3! Уже понятно, что в случае одного или нескольких повторений условия ( у < х) будет достаточно. Объединив это условие с условием ( у = х ), полученным лля нулевого числа повторений цикла, окончательно получим условие (у <= х), которое и будем использовать в качестве инварианта цикла.
Предусловие для оператора м)з11в можно определить из инварианта цикла. В нашем примере можно использовать условие Р = !. Мы должны убедиться, что наш выбор соответствует пяти критериям, упомянутым выше. Проверяем первый: поскольку Р = (, то Р =>!. Второе требование состоит в том, чтобы на инвариант цикла ! не оказывало влияния вычисление значения булевского выражения, которым в нашем случае является выражение у <> х. В этом выражении никакие значения не изменяются, так что на инвариант цикла ! оно также не влияет.
Далее, должно быть справедливым следующее выражение: (! ало' В) 5 (!) 158 Глава 3. Описание синтаксиса и семантики В нашем примере имеем: (у <= х апс] у <> х) у = у ' (у <= х) Применим к последнему выражению аксиому присваивания ууч1(у<=х] Тогда мы получим условие (у ь 1 <= х1, что эквивалентно условию:,у < х]. следующему из условий (у <= х] и (у <> х). Таким образом, привеленное выше утверждение доказано. Далее, должно быть справелливым условие (1 апд (пог В)) => 0 В нашем случае имеем ((у < х] апг] поС (у <> х)) => (у = х) ((у <= х) апс] поС (у х)) > (у = х) (у х) => (у = х) Эти утверждения, очевидно, истинны. Далее должно быть рассмотрено завершение цикла. В нашем примере, зто вопрос о том, завершается ли цикл (у < х] м)зд1е у <> х с(о у = у ь 1 епс) (у = х! Поскольку х и у предполагаются целыми числами, ясно. что число повторений цикла не бесконечно.
Предусловие гарантирует, что изначально значение переменной у не превышает значения переменной х. Каждое повторение тела цикла увеличивает значение переменной у до тех пор, пока оно не станет равным значению переменной х. Не важно, насколько изначально значение переменноЯ у было меньше значения переменной х, в конечном счете оба значения станут равными, т.е. выполнение цикла завершится. Поскольку наш выбор условия 1 удовлетворяет всем пяти поставленным критериям, то оно подходит на роль инварианта цикла и предусловия цикла. Описанный выше процесс вычисления инварианта цикла не всегда порождает утверждение, являюшееся слабейшим предусловием (хотя лля приведенного выше примера это было именно так).
В качестве другого примера нахождения инварианта цикла рассмотрим следуюший оператор цикла: м)зз1е в > 1 <)о в = в / 2 епс) (л - 1) Как и в описанном выше случае,мы используем аксиому присваивания для определения инварианта и предусловия цикла, Для нулевого числа повторов цикла слабейшим предусловием будет (в = 1). Для одного повтора: ер(в = в / 2, (в = 1)) = (в ! 2 = 1), или (в = 2) Для лвух повторов цикла: чр(в=в/2, (в=2)) = (в/2=2),или (в=4) Для трех: 3.6. Описание смысла программ: динамическая семантика 159 ир(з = з l 2, (з = 4)) = (з ! 2 = 4), или (з = 8) Таким образом, инвариант равен: (з — неотрицательная степень числа 2) Напомним, что вычисленный инвариант цикла ! может служить предусловием цикла Р и уловлетворяет пяти поставленным требованиям.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
