Р.У. Себеста - Основные копцепции языков программирования (2001) (1160794), страница 41
Текст из файла (страница 41)
Регистры, память, информация о состоянии и процесс выполнения операторов — все это можно моделировать. Набор команд можно создать так, чтобы семантику кажлой отдельной команды было легко понять и описать. Таким образом. машина была бы идеализирована и значительно упрощена, что облегчило бы понимание изменений ее состояния. Использование операционного метода лля полного описания семантики языка программирования Е требует создания двух компонентов.
Во-первых. лля преобразования операторов языка Ь в операторы выбранного языка низкого уровня нужен транслятор. Во-вторых, для этого языка низкого уровня необходима виртуальная машина, состояние которой изменяется с помощью команд, полученных при трансляции данного оператора языка высокого уровня. Именно изменения состояния этой виртуальной машины определяют смысл данного оператора. Основной процесс операционной семантики не является чем-то необычным. Фактически эта концепция часто используется в учебниках по программированию н справочниках по языкам программирования.
Семантику конструкции Еог языка С, например. можно описать в терминах следующих простых команд. Незначительное обобшение приведенных выше трех операгоров присваивания позволяет описывать более обшие арифметические выражения и операторы присваивания. 1(оные операторы выглядят следуюшич образом: -.'еп=: = чаг Ь-'и ос т а» . аегг:= цп ор чая Здесь о' и ор — бинарный арифметический оператор.
а цп ор — унарный оператор. Многочисленные арифметические типы данных и автоматическое преобразование пнюв. конечно, несколько усложняют зто обобшение. Введение небольшого количества новых относительно простых команд позволит описывать семантику массивов, записей, указателей и подпрограмль Семантика различных управляюших операторов с использованием операционной сечаитики описана в главе 7.
З.б.1.2. Оценка Первым и самым значительным использованисм формальной опсрашюнной семантики было описание семантики языка Р(Л (%ейпег. 1971). Эта абстрактная машина и правила трансляции языка РЫ были названы обшич именем Ч(еппа Е)ейпйюп (.апяцаяе (ЧО(.) в чссть города. в котором они были созданы корпорашмй 1ВМ. Операционная семантика является зффекгианой до тех пор. иола описание языка остается простым и неформальным. Е сожкзению, описание ЧО(. языка Р1/1 настолько сложно.
что пралтическим целям оно фактически не служит Операционная семантика зависит от атгоритчов. а не от л~атематики. Операторы одного языка программирования описываются в терминах операторов др)лого языка програччирования. имеющего более низкий уровень. Этот подход может привести к порочном) кругу, когда концепции неявно выражаются через самих себя.
Методы, описываемые в следуюших двух разделах. значительно более формальны в том смысле, что они опираются на логику и математику, а не на машины. 3.6.2. Аксиоматическая семантика Аксиоматичесьяя семантика (ах(оп1аг(с зеп1апцс1) была создана в процессе разработки л1етода доказательства правильности программ. (акис доказательства показывают, что программа выполняет вычисления, ошюанные ее спецификаш1ей. В локазательсзве каждый оператор программы сопровождается предшествуюшич и последующим логическими выражениями, устанавливаюшими ограничения на переьшнные в программе. Этн выражения используются для определения смысла оператора вмесзо полного описания состояния абстрактной машины (как в операционной сел1аитике).
В качестве формы записи используется исчисление предикатов. являюшееся фак1ич«ским языком аксиоматичсской семантики. Простыл булевских выражений не всегда бывает достаточно лля выражения ограничений. 3.6.2. 1. Утверждения Лксиоматическая семантика основана на математической логике. Логические выражения называются предикатами.
или утверждениями (аззеп(опз). Утверждение, непосредственно предшествующее оператору программы, описывает ограничения, наложенные на переменные в данном месте программы. Утверждение. следующее непосредственно за оператором программы, описывает новые ограничения на те же (а возможно, и Глава 3. Описания синтаксиса н семантики 1а2 другие) переменные после выполнения оператора. Эти утверждения называются соответственно прелусловием (ргесопсйгюп) и посттсловием (роз(сопгй6оп) оператора. РазраГютка аксиоматического описания или доказательства данной программы требует наличия у каждого оператора программы прелусловий и пост) еловой. В следуюших разделах прн из)чении утверждений мы будем предполагать, что предусловия операторов вычисляются на основе постусловий.
хотя этот процесс можно рассматривать и с противоположной точки зрения. Предположим. что все переменные являются целочисленными Рассмотрим в качестве примера оператор присваивания н постчсловие: вцж := ' х а"-... > Предусловия и пост) с.човия почешаются в фигурные скобки. зля того чтобы отличать их от операторов программы. Олпом из возможных прелусловий данного оператора может быть ( х: 10 (. 3.6.2.2. Слабейшие пред условия Слабейшими предусловиями (кгеа(гезг ргесопгййопз) называются наименьшие предусловия. обеспечивающие выполнение соотаетствуюшего постусловия.
Например. шзя привеленного выше оператора и его постусловия прелусловия ° х > 10). х > 00; и ( х > 1000' являются правильными. Слабейшим из всех предусловий в данном случае будет (х . 0;. Если зля каждого оператора языка по заданным постусловиям можно вычислить слаГ1ейшее предусловие. то лля программ на данном языке может быть построено корректное доказательство. Доказательство начинается с использования рез)льтатов. которые надо получить при выполнении программы. в качестве постусловия последнего оператора программы, и выполняется с помошью отслеживания программы от конца к начазу с последовательным вычислением слабейших прелусловий для каждого оператора. При достижении начала программы первое ее презусловие отражает условия.
при которых программа вычислит требуемые результаты. Для некоторых операторов программы вычисление слабейшего предусловия на основе оператора и его постусловия является достаточно простым и может быть задано с помошью аксиомы. Однако в большинстве случаев слабейшее предусловие вычисляется только с помошью правила логического вывода. Аксиомой (ахюгп) называется логический оператор, прелполагаемый истинным; правилом логического вывода ((пГегепсе гц!е) является метод выведения истинности одного утверждения на основе значений остальных утверждений. Чтобы использовать аксиоматическую семантику с данным языком программирования для доказательства правильности программ или для описания формальной семантики.
для каждого вида операторов языка должны быть определены аксиомы или правила логического вывода. В следуюших подразделах мы приводим аксиому для операторов присваивания и правила логического вывода лля последовательности операторов. операторов ветвления н логически управляемых циклов с прелусловиями. З.б.2.3. Слзеретеры присваивания Пусть х = Š— обычный оператор присваивания, а () — его постусловие. Тогда предусловие Р того же оператора опрелеляется аксиомой Р=О а 153 3.6.
Описание смысла программ: динамическая семантика Эта аксиома означает, что предусловие Р вычисляется как условие О, в котором все переменные х заменены переменными Е. Пусть, например, есть оператор присваивания н посттсловие а = Ь / 2 -1 (а < 10) Тогда слабейшее прелусловие вычисляется подстановкой Ь / 2 — 1 в утверждение а < 101: Ь / 2 -1 < 10 Ь . 22 Таким образом, слабейшим предусловием для данных оператора и его постусловия является (Ь < 22). Отметим, что истинность аксиомы присваивания гарантируется только при отсутствии побочных эффектов. Побочный эффект оператора присваивания может проявляется, если оператор изменяет значения переменных, не входящих в его левую часть. Ниже прелставлена обычная запись лля задания аксиоматической семантики данного оператора: (Р)5(О), где Р— прелусловие, Π— постусловие, а Б — операторная форма.
Для оператора присваивания форма записи такова: (О„е) х = Е (О) Рассмотрим другой пример вычисления предусловия лля оператора присваивания: х = 2 * у — 3 (х > 25) В данном случае предусловие вычисляется слелующим образом: 2у-3>25 у> 14 Следовательно, (у > 14) — слабейшее предусловие при заданных операторе присваивания и его постусловии. Отметим, что появление левой части оператора присваивания в его правой части не влияет на процесс вычисления слабейшего предусловия. Например, для оператора х = х + у — 3 (х > 10) слабейшим предусловием является х+у — 3>10 у>13-х В начале нашего обсуждения мы утверждали, что аксиоматическая семантика была разработана лля доказательства правильности программ. В свете этого утверждения естественным будет поинтересоваться, как вообще аксиома для оператора присваивания может использоваться для доказательства чего-либо.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
