Р.У. Себеста - Основные копцепции языков программирования (2001) (1160794), страница 43
Текст из файла (страница 43)
Однако в отличие от предыдущего примера поиска предусловия цикла найденное условие отнюдь не является слабейшим Рассмотрим использование предусловия (а > 1). Можно легко доказать логическое выражение (а > 1) мц11в а > 1 с(о а = а l 2 епс) (в = 1) Это предусловие значительно шире предусловия, найденного выше. Цикл и прелусдовие удовлетворяются любым положительным значением переменной а, а не только степенью двойки, как было показано ранее. В силу правила логического следствия использование предусловия, более сильного, чем слабейшее предусловие, не опровергает доказательства.
Найти инварианты цикла не всегда легко. Для этого следует понять их природу. Вопервых, инвариант цикла является ослабленным вариантом постусловия и одновременно предусловием цикла. Таким образом, условие ! должно быть лостаточно слабым лля удовлетворения его в начале выполнения цикла, но в то же время в сочетании с условием выхода из цикла оно должно быть достаточно сильным, чтобы гарантировать истинность постусловия. Вследствие трудности доказательства завершения цикла это условие часто просто игнорируется.
Если завершение цикла может быть показано, то аксиоматическое описание цикла называется локазательством полной корректности (го)а! сопес!пезз). Если остальные условия удовлетворены, но завершение цикла не гарантировано, то такое описание называется доказательством частичной корректности (рагйа! соггесюезз). Поиск подходяшего инварианта в более сложных циклах даже для доказательства его частичной корректности требует известной доли изобретательности. Поскольку поиск предусловия для цикла мЬ11в зависит от обнаружения инварианта цикла, то доказательство с использованием аксиоматической семантики правильности программ, содержаших подобные циклы, может оказаться сложным.
Ниже следует пример доказательства правильности программы, написанной на псевдоколе и вычисляюшей факториал. гп >= 0) счетчик = п; факториал = 1; иЬ11е счетчик <> 0 с)о факториал = факториал * счетчик; счетчик = счетчик — 1; а ',факториал = и!) Описанный выше метод нахождения инварианта цикла не подходит для цикла в данном примере. Здесь требуется определенная находчивость. проявлению которой поможет краткое изучение программы.
Данный цикл вычисляет факториал, начиная с последнего множителя: т.е. первым выполняется умножение (и — 1) * л (предполагается, что г больше единицы). Таким образом, частью инварианта может быть 160 Глава 3. Описание синтаксиса и семантики факториал (счетчик + 1) * (счетчик + 2)* ... * (и — 1; и Однако мы также лолжны гарантировать, чтобы переменная счетчик всегда была неотрицательной. Для этого следует добавить требуемое условие к полученной выше части: 1 = (факториал = (счетчик + 1) * ... * п) АЫ0 (счетчик >= О) Затем надо проверить, чтобы условие ! удовлетворяло требованиям, предъявляемым инварнантам. Снова используем условие ! в качестве условия Р, таким образом.
из условия Р будет явно следовать условие !. Вычисление булевского выражения оператора иЬД1е (в данном случае счетчик <> О), очевидно, никак не повлияет на условие !. Следующий вопрос, требующий доказательства: (!иВ) ЗЩ Условие(! апд В) означает: ((факториал (счетчик + 1) * ... ~ и) АЫ0 (счетчик >= О)) А](0 (счетчик <> О) В упрощенном виде можно эаписатгк (факториал = (счетчик + 1) * ...
* п] А]!О (счетчик > О) В нашем случае мы должны вычислить предусловие тела цикла, используя значение инварианта для постусловия. Для условия (Р) счетчик счетчик — 1 (1) мы находим, что условие Р имеет вил ( (факториал счетчик * (счетчик + 1) * ... * п] АЬ]0 (счетчик > 1) ) Используем это в качестве постусловия дяя первого присваивания в теле цикла (Р) факториал = Факториал * счетчик ((факториал = счетчик * (счетчик + 1] * ... * и) А](0 (счетчик >= 1)] В этом случае условием Р будет следующее ((факториал (счетчик + 1) * ...
* п) А!ч0 (счетчик >= 1)] Очевидно, что из условий ! и В слелует условие Р, т.е. по правилу логического следствия утверждение (! А)ЧО В» Б Щ истинно. Последняя проверка условия 1: ! А]ЧО (]чОТ В) > О Для нашего примера это означает ((факториал (счетчик + 1) * ... * и) АМ0 (счетчик >= О) ) АЬ]0 (счетчик = О) => факториал = и! 161 3,6. Описание смысла программ: динамическая семантика Это. очевидно, истинно при значении переменной счетчик = О, таким образом, первая часть является в точности определением факториала.
Итак, наш выбор условия ) удовлетворяет всем требованиям, предъявляемым инвариантам цикла. Теперь мы можем использовать условие Р (аналогнчное условию!) лля цикла с условием иЬ11е в качестве постусловия второго присваивания программы: (Р) факториал = 1 ((факториал (счетчик + 1) ъ ... " п) А(Ч(З (счетчик >= О)] Из него вытекает следующее значение условия Р: ( (1 = (счетчик + 1) * ...* п) АЫР (счетчик >= О) ) Используем это в качестве постусловия первого присваивания программы (Р) счетчик = п ((1 (счетчик + 1) + ...
* п) Ай0 (счетчик > О]) Тогда мы получим следующее значение условия Р: (((и + 1) * ... п 1) А(Ч0 (и > О) ) Левый операнл оператора А(Ч0 истинный (поскольку 1 = 1), а правый операнд в точности равен прелусловию всего фрагмента программы ( и >- 0 ). Следовательно, правильность программы доказана. 3.6.2.7. Оценка При определении семантики полного языка программирования с использованием аксиоматического метода для каждого вила операторов языка должны быть сформулированы аксиома или правило логического вывода.
Доказано, что определение аксиом и правил логического вывода для некоторых операторов языков программирования— очень сложная задача. Напрашивающимся решением такой проблемы является разработка языка, полразумеваюшего использование аксиоматического метода, т.е. содержащего только те операторы, для которых могут быть написаны аксиомы или правила логического вывода.
К сожалению, подобный язык оказался бы слишком маленьким и простым, что отражает нынешнее состояние аксиоматической семантики как науки. Аксиоматическая семантика является мощным инструментом дяя исследований в области доказательств правильности программ, она также создает великолепную основу для анализа программ, как во время их создания, так и позднее. Однако ее полезность при описании содержания языков программирования весьма ограничена как для пользователей языка, так и для разработчиков компиляторов. 3.6.3.
Денотоционноя седйонтико Деиотацнонная семантика (депоцп)опа! вешапбсз) — самый строгий широко известный метод описания значения программ. Она прочно опирается на теорию рекурсивных функций. Всестороннее рассмотрение денотационной семантики — длительное и сложное дело. Мы намереваемся ознакомить читателя лишь с ее основными принципами. Основной концепцией денотацнонной семантики является определение для каждой сущности языка некоего математического объекта и некоей функции, отображающей экземпляры этой сущности в экземпляры этого математического объекта.
Поскольку объекты определены строго, то они представляют собой точный смысл соответствующих им Глава 3. Описание синтаксиса и семантики 162 сущностей. Сама идея основана на факте существования строгих методов оперирования математическими объектами, а не конструкциями языков программирования. Сложность использования этого метода заключается в создании объектов и функций отображения.
Название метода "денотационная семантика" происходит от английского слова Непоге (обозначать), поскольку математический объект обозначает смысл соответствующей синтаксической сущности. 3.6.3.!. Деа простых примера Для введения в денотационный метод мы используем очень простую языковую конструкцию — двоичные числа. Синтаксис этих чисел можно описать следующими грамматическими правилами: <двоичное число> -ь О 1 1 1 <двоичное число> О 1 <двоичное число> 1 На рис. 3.10 показано дерево синтаксического анализа для выбранного в качестве примера двоичного числа 110. Рис. л. 10.
Дерева сингнаксического анализа двоичного числа 1! 0 Для описания двоичных чисел с использованием денотационной семантики и грамматических правил, указанных выше, их фактическое значение связывается с каждым правипом, имеющим в своей правой части один терминальный символ.
Объектами в данном случае являются десятичные числа. В нашем примере значащие объекты должны связываться с первыми двумя грамматическими правилами. Остальные два правила являются, в известном смысле. правилами вычислений, поскольку они объединяют терминальный символ, с которым может ассоциироваться объект, с нетерминальным, который может представлять собой некоторую конструкцию.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
