Теория вычислительных процессов
Лекция 6
назад | содержание | вперед

Лекция 6

2. СЕМАНТИЧЕСКАЯ ТЕОРИЯ ПРОГРАММ

2.1. Описание смысла программ

Существует несколько причин, по которым следует заниматься описанием семантики программ, - смысла выражений, операторов и программных единиц.

Руководство по использованию языка программирования должно включать описание каждой конструкции языка, как по отдельности, так и в совокупности с другими конструкциями. В языке имеется множество различных конструкций, точное определение которых необходимо как программисту, использующему язык, так и разработчику реализации этого языка. Программисту эти сведения нужны для того, чтобы писать правильные программы и заранее знать результат вьполнения любых операторов программы. Разработчику компилятора корректные определения конструкций необходимы для создания правильной реализации языка.

В большинстве руководств определение семантики дается в виде обычного текста. Как правило, сначала при помощи какой-либо формальной грамматики дается определение синтаксиса конструкции, а затем для пояснения семантики приводятся несколько примеров и небольшой пояснительный текст. К сожалению, смысл этого текста часто неоднозначен, так что разные читатели могут понимать его по-разному. Программист может получить ошибочное представление о том, что именно будет делать написанная им программа при вьполнении, а разработчик может реализовать какую-либо языковую конструкцию иначе, чем разработчики других реализаций того же языка. Как и для синтаксиса, нужен какой-то метод, позволяющий дать удобочитаемое, точное и лаконичное определение семантики языка. .

Задача определения семантики языка программирования рассматривается теоретиками давно. Но до сих пор не найдено удовлетворительного универсального решения. Было разработано множество различных методов формального определения семантики. Ниже приводятся описания некоторых из них.


2.1.1. Операционная семантика

Операционная семантика сводится к описанию смысла программы посредством выполнения ее операторов на реальной или виртуальной машине. Смысл оператора определяется изменениями, произошедшими в состоянии машины после выполнения данного оператора. Для того чтобы разобраться в этой концепции, рассмотрим команду на машинном языке. Пусть состояние компьютера - это значения всех его регистров и ячеек памяти, в том числе коды условий и регистры состояний. Если просто записать состояние компьютера, выполнить команду, смысл которой нужно определить, а затем изучить новое состояние машины, то семантика этой команды станет понятной. Она представляется изменением в состоянии компьютера, вызванным выполнением команды.

Описание операционной семантики операторов языков программирования высокого уровня требует создания реального или виртуального компьютера. Аппаратное обеспечение компьютера является чистым интерпретатором его машинного языка. Чистый интерпретатор любого языка программирования может быть создан с помощью программных средств, которые становятся виртуальным компьютером для данного языка. Семантику языкa высокого уровня можно описать, используя чистый интерпретатор данного языка. При таком подходе, правда, существуют две проблемы. Во-первых, сложность и индивидуальные особенности аппаратного обеспечения компьютера и операционной системы, используемых для запуска чистого интерпретатора, затрудняют понимание происходящих действий. Во-вторых, вьполненное таким образом семантическое определение будет доступно только для людей с абсолютно идентичной конфигуpацией компьютера.

Этой проблемы можно избежать, заменив реальный компьютер виртуальным компьютером низкого уровня. Регистры, память, информация о состояниии процесса выполнения операторов - все это можно смоделировать соответствующими программами. Набор команд можно создать так, чтобы семантику каждой отдельной команды можно легко понять и описать. Таким образом, машина была бы идеализирована и значительно упрощена, что облегчило бы понимание изменений ее состояния.

Использование операционного метода для полного описания семантики языка программирования L требует создания двух компонентов. Во-первых, для преобразования языка L в операторы выбранного языка низкого уровня нужен транслятор. Во-вторых, для этого языка низкого уровня необходима виртуальная машина, состояние которой изменяется с помощью команд, полученных при трансляции операторов высокого уровня. Именно изменения состояния этой виртуальной машины определяет смысл данного оператора.

Семантику конструкции for языка Си можно описать в терминах следующих простых команд.

Человек, читающий подобное описание, является “виртуальным компьютером” и предполагается способным правильно “вьполнить” команды описания и распознать эффект такого “выполнения”.

В качестве примера низкоуровневого языка, который можно применять для операционной семантики, рассмотрим список операторов, соответствующих простым управляющим операторам типичного языка программирования:

ident := var

ident := ident - 1

goto label

if var relop var goto label

Здесь геlор-один из операторов отношений из набора {=, <>, >, <, >=, <=},

ident - идентификатор, а var -- идентификатор или константа. Все эти операторы просты и легки для понимания и реализации.

Незначительное обобщение приведенных выше трех операторов присваивания позволяет описывать более общие арифметические выражения и операторы присваивания. Например:

ident := var bin_ор var

ident := un_ор var

Здесь bin_ор - бинарный арифметический оператор, а un_ор – унарный оператор. Многочисленные арифметические типы данных и автоматическое преобразование типов, конечно, несколько усложняют это обобщение. Введение небольшого количества новых относительно простых команд позволит описывать семантику массивов, записей, указателей и подпрограмм.

Описание операционной семантики функций рассмотрим на примере системы равенств:

f1(x1, x2, ... , xk)= Е1,

f2(x1, x2, ... , xk)= Е2,

f3(x1, x2, ... , xk)= Ез, (2.1)

…………………………

fm(x1, x2, ... , xk)= Еm,

где в левых частях равенств явно указаны определяемые функции с формальными параметрами, включающими обозначения всех входных данных x1, x2,,,, , xk, а правые части представляют собой выражения, содержащие, вообще говоря, вхождения этих функций с аргументами, задаваемыми некоторыми выражениями, зависящими от входных данных x1, x2, ... , хk.

Операционная семантика интерпретирует эти равенства как систему подстановок. Под подстановкой <s, Е, t> терма t в выражение Е вместо символа s (в частности, переменной) будем понимать переписывание выражения Е с заменой каждого вхождения в него символа s на выражение t. Каждое равенство fi(x1, x2, ... , хk) = Ei задает в параметрической форме множество правил подстановок:

<x1, x2, ... , хk; fi(t1, t2, ... , tk) -> Ei; t1, t2, ... , tk>

где t1, t2, … ,tk - конкретные аргументы (значения или определяющие их выражения) данной функции. Это правило допускает замену вхождения левой его части в какое-либо выражение на его правую часть.

Интерпретация системы равенств (2.1) для получения значений определяемых функций в рамках операционной семантики производится следующим образом. Пусть задан набор входных данных (аргументов) d1, d2, … , dk. На первом шаге осуществляется подстановка этих данных в левые и правые части равенств с выполнением там, где это возможно, предопределенных операций и с выписыванием получаемых в результате этого равенств. На каждом следующем шаге просматриваются правые части полученных равенств. Если правая часть является каким-либо значением, то оно и является значением функции, указанной в левой части этого равенства. В противном случае, правая часть является выражением, содержащим вхождения каких-либо определяемых функций с теми или иными наборами аргументов. Если для такого вхождения соответствующая функция с данным набором аргументов имеется в левой части какого-либо из полученных равенств, то либо вместо этого вхождения подставляется вычисленное значение правой части этого равенства, либо не производится никаких изменений. В том же случае, если эта функция с данным набором аргументов не является левой частью ни какого из полученных равенств, то формируется (и дописывается к имеющимся) новое равенство. Оно получается из исходного равенства для данной функции подстановкой в него вместо параметров указанных аргументов этой функции. Такие шаги осуществляются до тех пор, пока все определяемые функции не будут иметь вычисленные значения.

Первым и самым значительным использованием формальной операционной семантики было описание семантики языка PL/I. Эта абстрактная машина и правила трансляции языка PL/I были названы общим именем Vienna Definition Language (VDL) в честь города, в котором они были созданы корпорацией IBM.

Операционная семантика является эффективной до тех пор, пока описание языка остается простым и неформальным. К сожалению, описание VDL языка PL/I настолько сложно, что практическим целям оно фактически не служит.

Операционная семантика зависит от алгоритмов, а не от математики. Операторы одного языка программирования описываются в терминах операторов другого языка программирования, имеющего более низкий уровень. Этот подход может привести к порочному кругу, когда концепции неявно выражаются через самих себя. Методы, описываемые в следующих двух разделах, значительно более формальны в том смысле, что они опираются на логику и математику, а не на машины.


2.1.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}.


2.1.2.1. Преобразователь предикатов

Э. Дейкстра рассматривает слабейшие предусловия, т.е. предусловия, необходимые и достаточные для гарантии желаемого результата.

“Условие, характеризующее множество всех начальных состояний, при которых запуск обязательно приведет к событию правильного завершения, причем система (машина, конструкция) останется в конечном состоянии, удовлетворяющем заданному постусловию, называется слабейшим предусловием, соответствующим этому постусловию”.

Условие называют слабейшим, так как чем слабее условие, тем больше состояний удовлетворяют ему. Наша цель - охарактеризовать все возможные начальные состояния, которые приведут к желаемому конечному состоянию.

Если 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 и предикатов Р и R таких, что Р => R для всех состояний, справедливо для всех состояний wp(S, Р) => wp(S, R).

Свойство 3. Дистрибутивность конъюнкции. Для любых S, Р, R справедливо

wp(S, Р) AND wp(S, R) = wp(S, Р AND R).

Свойство 4. Дистрибутивность дизыокции.. для любых S, Р, R справедливо

wp(S, Р) OR wp(S, R) = wp(S, Р OR R).

Если для каждого оператора языка по заданным постусловиям можно вычислить слабейшее предусловие, то для программ на данном языке может быть построено корректное доказательство. Доказательство начинается с использования результатов, которые надо получить при выполнении программы, в качестве постусловия последнего оператора программы, и вьполняется с помощью отслеживания программы от конца к началу с последовательным вычислением слабейших предусловий для каждого оператора. При достижении начала программы первое ее предусловие отражает условия, при которых программа вычислит требуемые результаты.

Для некоторых операторов программы вычисление слабейшего предусловия на основе оператора и его постусловия является достаточно простым и может быть задано с помощью аксиомы. Однако, как правило, слабейшее предусловие вычисляется только с помощью правила логического вывода, т.е. метода выведения истинности одного утверждения на основе значений остальных утверждений.


2.1.2.2. Аксиоматическое определение операторов в терминах wp

Определим слабейшее предусловие для основных операторов: оператора присваивания, составного оператора, оператора выбора и оператора цикла.

Оператор присваиванuя имеет вид: х:= Е, где х - простая переменная, Е выражение (типы х и Е совпадают).

Определим слабейшее предусловие оператора присваивания как Q = wp(x:= Е, R), где Q получается из R заменой каждого вхождения х на Е.

Предполагается, что значение Е определено и вычисление выражения Е не может изменить значения ни одной переменной. Последнее ограничение запрещает функции с побочным эффектом. Следовательно, можно использовать обычные свойства выражений такие, как ассоциативность, коммутативность и логические законы.

Составной оператор имеет вид: begin S1; S2; ... ; Sn end

Слабейшее предусловие для последовательности двух операторов:

wp(S1;S2; R) = wp(S1,wp(S2, R)).

Аналогично, слабейшее предусловие определяется для последовательности из n операторов.

Оператор выбора определим так: if B1 ->S1 П В2 ->S2... П Вn ->Sn fi

Здесь n >= 0, В1, В2, ..., Вn - логические выpажения, называемые охранами,

S1, S2, ..., Sn - операторы, пара Bi -> Si называется охраняемой командой, П - разделитель, if и fi играют роль операторных скобок.

Выполняется оператор следующим образом.

Проверяются все Bj. Если одна из охран не определена, то происходит аварийное завершение. Далее, по крайней мере, одна из охран должна иметь значение истина, иначе выполнение завершается аварийно.

Выбирается одна из охраняемых команд Bj -> Sj, у которой значение Bj истина, и выполняется Sj.

Определим слабейшее предусловие:

wp(if, R) = ВВ AND1 => wp(S1, R)) AND ... ANDn => wр(Sn, R)),

где ВВ = В1 OR В2 OR ... OR Вn.

Предполагается, что охраны являются всюду определенными функциями (значение их определено во всех состояниях).

Естественно определить wp(if, R) с помощью кванторов:

wp(if, R) = (i: 1 <= i<= n : Bi ) AND (i: 1 <=i<= n : Вi => wp(Si, R))

Пример 2.4. Определить z = |х|.

С использованием оператора выбора :if x 0 -> z := х П х 0 -> z := -x fi.

К особенностям оператора выбора следует отнести, во-первых, тот факт, что он включает условный оператор (if... then..), альтернативный оператор (if... then... else...) и оператор выбора (case).

Во-вторых, оператор выбора не допускает умолчаний, что помогает при разработке сложных программ, так как каждая альтернатива представлена подробно, и возможность что-либо упустить уменьшается.

В-третьих, благодаря отсутствию умолчаний, запись оператора выбора представлена в симметричном виде.

Операmор цикла. В обозначениях Дейкстры цикл имеет вид: do В -> S do.

Обозначим это соотношение через DО и представим его в виде:

DO: do В1-> S1 П B2 -> S2 ... П Вn -> Sn od,

где n 0, Bi -> Si - охраняемые команды.

Выполняется оператор следующим образом. Пока возможно выбирается охрана Вj со значением истина, и выполняется соответствующий оператор Sj. Как только все охраны будут иметь значение ложь, выполнение DO завершится.

Выбор охраны со значением истина и выполнение соответствующего оператора называется выполнением шага цикла. Если истинными являются несколько охран, то выбирается любая из них.

Следовательно, оператор D0 эквивалентен оператору

ВВ -> if B1 ->S1 П В2 -> S2 … П Вn -> Sn fi оd

или ВВ -> IF оd,

где ВВ - дизъюнкция охран, IF - оператор выбора.

Пример 2.5. Алгоритм Евклида.

Вариант 1.

задать (N, М);

if N > 0 AND М > 0 ->n, m := N, М;

n <> m -> if n > m -> n := n – m П m> n -> m := m - n fi оd;

выдать (n)

fi

Вариант 2.

задать (N, М);

if N> 0 AND M> 0 ->n, m :=N,M;

n > m -> n := n - m П m > n -> m := m - n do;

выдать (n)

fi

Дадим формальиое определение слабейшего предусловия для оператора цикла DO.

Пусть предикат H0(R) определяет множество состояний, в которых вьполнение DO завершается за 0 шагов (в этом случае все охраны с самого начала ложны, после завершения R имеет значение истина):

H0(R) = NOT ВВ AND R

Другими словами, требуется, чтобы оператор цикла DO завершил работу, не производя выборки охраняемой команды, что гарантируется первым конъюнктивным членом предиката H0(R): NOT ВВ = Т. При этом истинность R до вьполнения DO является необходимым условием для истинности R после выполнения DO.

Определим предикат Hk(R) как множество состояний, в которых выполнение DO заканчивается за k шагов при значении R истина (Нk(R) будет определяться через Нk-1(R)):

Hk(R) = Н0(R) OR wp(IF, Hk-1(R)), k> 0 -> wp(DO, R) = (V k: k >=0: Hk(R)).

Это значит, что должно существовать такое значение k, что потребуется не более, чем k шагов, для обеспечения завершения работы в конечном состоянии, удовлетворяющем постусловию R.

Определение DO. Если предикаты Hk(R) задаются в виде

Hk(R) = NOT В AND R, k = 0

Hk(R) = wp(IF, Hk-1(R)), k> 0, -> wp (DO,R)=( k: k 0: Hk(R))

Основная теорема для оператора цикла. Пусть оператор выбора IF и предикат Р таковы, что для всех состояний справедливо

AND ВВ) => wp(IF, R). (2.3)

Тогда для оператора цикла справедливо: (P AND wp(DO, Т)) => wp(DO, Р AND NOT BB).

Эта теорема известна как основная теорема инвариантности для цикла.

Предикат Р, истинный перед выполнением и после выполнения каждого шага цикла, называется инвариантным отношением или просто инвариантом цикла. В математике термин “инвариантный” означает не изменяющийся под воздействием совокупности рассматриваемых математических операций.

Поясним смысл теоремы. Условие (2.3) означает, что если предикат Р первоначально истинен и одна из охраняемых команд выбирается для выполнения, то после ее выполнения Р сохранит значение истинности. После завершения оператора, когда ни одна из охран не является истиной, будем иметь:

Р AND NOT ВВ.

Работа завершится правильно, если условие wp(DO, Т) справедливо и до вьполнения DO. Так как любое состояние удовлетворяет Т, то wp(DО,Т) является слабейшим предусловием для начального состояния такого, что запуск оператора цикла DO приведет к правильно завершаемой работе.

Доказательство. Из определения DO следует:

Если H0(Т)= NOT ВВ AND Т, k=0

Hk(T)=wp(IF, Hk-1(T)), k>0, -> wp(DO,T)=( k: k 0: Hk(T))

H0AND NOT ВВ)=Р AND NOT ВВ;

Hk(P AND NOT BB)=wp(IF, Hk-1(P AND NOT ВВ), ->

-> wp(DO, Р AND NOT ВВ)=( k 0: Hk(P AND NOT ВВ))

С помощью метода математической индукции можно доказать, что из условия (2.3) следует

AND Hk(T)) => Hk(P AND NOT ВВ), k 0

Тогда имеем

Р AND wp(DO, Т) = (k: k 0: Р and Hk(T)) =>

=> (k: k 0: Hk(P AND NOT ВВ)) = wp(DO, Р AND NOT ВВ).

Следовательно, (Р AND wp(DO, Т)) => wp(DO, Р AND NOT ВВ).

Чтобы использовать аксиоматическую семантику с данным языком программирования для доказательства правильности программ или для описания формальной семантики, для каждого вида операторов языка должны быть определены аксиомы или правила логического вывода. С ними мы познакомимсяв п. 2.3 “Верификация программ”.

В аксиоматической семантике система (2.1) интерпретируется как набор аксиом в рамках некоторой формальной логической системы, в которой есть правила вывода и/или интерпретации определяемых объектов.

Для интерпретации системы функций (2.1) вводится понятие аксиоматического описания <S, А> - логически связанной пары понятий: S - сигнатура используемых в системе символов функций f1, f2, ..., fm и символов констант (нульместных функциональных символов) c1, с2 ..., сi , а А - набор аксиом, представленный системой. Предполагается, что каждая переменная xi, i=l, ..., k, и каждая константа ci, i=l, ..., 1, используемая в А, принадлежит к какому-либо из типов данных t1, t2 ..., ti, а каждый символ fj, j=l, ..., m, представляет функцию, типа: ti1, ti2 ,…, . tik -> ti0. Такое аксиоматическое описание получит конкретную интерпретацию, если будут заданы конкретные типы данных ti= ti, i=1, ..., r, и конкретные значения констант сi = сi, i = 1, ...,1.

К. Хоар построил аксиоматическое определение набора типов данных, которые потом Н. Вирт использовал при создании языка Паскаль.

Пример 2.6. Рассмотрим систему равенств:

УДАЛИТЬ (ДОБАВИТЬ(m,d))=m,

ВЕРХ (ДОБАВИТЬ(m,d))=d,

УДАЛИТЬ (ПУСТ)=ПУСТ,

ВЕРХ (ПУСТ)=ДНО,

где УДАЛИТЬ, ДОБАВИТЪ, ВЕРХ - символы функций, а ПУСТ и ДНО - символы констант, образующие сигнатуру этой системы. Пусть D, Dl и М - некоторые типы данных, такие, что m М, d D, ПУСТ М, ДНО Dl, а функциональные символы представляют функции следующих типов:

УДАЛИТЬ: M->M,

ДОБАВИТЬ: М, D -> М,

ВЕРХ: M->Dl.

Данная сигнатура вместе с указанной системой равенств, рассматриваемой как набор аксиом, образует аксиоматическое описание абстрактного типа данных, называемого магазином.

Зададим интерпретацию символов ее сигнатуры: D - множество значений, которые являются элементами магазина, М - множество состояний магазина, М = {d1,d2, ... ,dn: di D, i=l, ..., n, n 0}, Dl=D {ДНО}, ПУСТ={}, а ДНО особое значение (зависящее от реализации магазина), не принадлежащее D. Тогда указанный набор аксиом определяют свойства магазина.

При определении семантики полного языка программирования с использованием аксиоматического метода для каждого вида операторов языка должны быть сформулированы аксиома или правило логического вывода. Но определение аксиом и правил логического вывода для некоторых операторов языков программирования - очень сложная задача. Трудно построить “множество основных аксиом, достаточно ограниченное для того, чтобы избежать противоречий, но достаточно богатое для того, чтобы служить отправной точкой для доказательства утверждений о программах” (Э. Дейкстра).

Напрашивающимся решением такой проблемы является разработка языка, подразумевающего использование аксиоматического метода, т.е. содержащей только те операторы, для которых могут быть написаны аксиомы или правила логического вывода. К сожалению, подобный язык оказался бы слишком маленьким и простым, что отражает нынешнее состояние аксиоматической семантики как науки.

Аксиоматическая семантика является мощным инструментом для исследований в области доказательств правильности программ. Она также создает великолепную основу для анализа программ, как во время их создания, так и позднее. Однако ее полезность при описании содержания языков программирования весьма ограничена как для пользователей языка, так и для разработчиков компиляторов.


2.1.3. Денотационная семантика

Денотационная семантика - самый строгий широко известный метод описания значения программ. Она прочно опирается на теорию рекурсивных функций. Всестороннее рассмотрение денотационной семантики – длительное и сложное дело. Здесь мы познакомимся лишь с ее основными принципами.

Основной концепцией денотационной семантики является определение для каждой сущности языка некоего математического объекта и некоей функции, отображающей экземпляры этой сущности в экземпляры этого математического объекта. Поскольку объекты определены строго, то они представляют собой точный смысл соответствующих сущностей. Сама идея основана на факте существования строгих методов оперирования математическими объектами, а не конструкциями языков программирования. Сложность использования этого метода заключается в создании объектов и функций отображения. Название метода “денотационная семантика” происходит от английского слова denote (обозначать), поскольку математический объект обозначает смысл соответствующей синтаксической сущности.

Для введения в денотационный метод мы используем очень простую языковую конструкцию - двоичные числа. Синтаксис этих чисел можно описать следующими грамматическими правилам

Для описания двоичных чисел с использованием денотационной семантики и грамматических правил, указанных выше, их фактическое значение связывается с каждым правилом, имеющим в своей правой части один терминальньrй (основной) символ. Объектами в данном случае являются десятичные числа.

В нашем примере значащие объекты должны связываться с первыми двумя правилами. Остальные два правила являются, в известном смысле, правилами вычислений, поскольку они объединяют терминальный символ, с которым может ассоциироваться объект, с нетерминальным, который может представлять собой некоторую конструкцию.

Пусть область определения семантических значений объектов представляет собой множество неотрицательных десятичных целых чисел Nat. Это именно те объекты, которые мы хотим связать с двоичными числами. Семантическая функция Мb отображает синтаксические объекты в объекты множества Nat согласно указанным выше правилам и определяется следующим образом:

Мd('0') = 0, Мd('1')=1

Md( <двоичное_ число> '0') = 2 * Md( <двоичное_число>)

Md( <двоичное_число> '1 ')= + 2 * Md( <двоичное_числ>) + 1

Синтаксические цифры заключены в апострофы, чтобы отличать их от математических цифр. Oтношение между этими категориями подобно отношениям между цифрами в кодировке АSCII и математическими цифрами. Когда программа считывает число как строку, то прежде, чем это число сможет использоватъся в программе, оно должно быть преобразовано в математическое число.


Пример 2.7. Описание значения десятичных синтаксических литеральных констант.

<десятичное_число> -> 0I1I2I3I4I5I6I7I8I9

<десятичное_число> (0I1I2I3I4I5I6I7I8I9)

Денотационные отображения для этих синтаксических правил имеют следующий вид:

Мd('0') = 0, Мd('1') = 1, …, Мd('9') = 9

Мd( <десятичное_число> '0') = 10 * Мd( <двоичное_число>)

Md(<десятичное_число> '1') = 10 * Мd(<десятичное _число>) + 1

Md(<десятичное_число>’9’)=10*Md(<десятичное_число>)+9

Денотационную семантику программы можно определить в терминах изменений состояний идеального компьютера. Подобным образом определялись операционные семантики, приблизительно так же определяются и денотационные. Правда, для простоты они определяются только в терминах значений всех переменных, объявленных в программе. Операционная и денотационная семантики различаются тем, что изменения состояний в операционной семантике определяются запрограммированными алгоритмами, а в денотационной семантике они определяются строгими математическими функциями. Пустъ состояние s программы определяется следующим набором упорядоченных пар:

{<i1, V1>, <i2, V2>, ..., <in, Vn>}.

Каждый параметр i является именем переменной, а соответствующие параметры V являются текyщими значениями данных переменных. Любой из параметров V может иметь специальное значение undef, указывающее, что связанная с ним величина в данный момент не определена.

Пусть VARМAP - функция двух параметров, имени переменной и состояния программы. Значение функции VARМAP(ik, s) равно Vk (значение, соответствующее параметру ik в состоянии s).

Большинство семантических функций отображения для программ и программных конструкций отображают состояния в состояния. Эти изменения состояний используются для определения смысла программ и программных конструкций. Отметим, что такие языковые конструкции, как выражения, отображаются не в состояния, а в величины.

Выражения являются основой большинства языков программирования. Более того, мы имеем дело только с очень простыми выражениями. Единственными операторами являются операторы + и *; выражения могут содержать не более одного оператора; единственными операндами являются скалярные переменные и целочисленные литеральные константы; круглые скобки не используются; значение выражения является целым числом. Ниже следует описание этих выражений в форме БНФ:

Единственной рассматриваемой нами ошибкой в выражениях является неопределенное значение переменной. Разумеется, могут появляться и другие ошибки, но большинство из них зависят от машины. Пусть Z - набор целых чисел, а error - ошибочное значение. Тогда множество Z u {error} является множеством значений, для которых выражение может бьrть вычислено.

Ниже приведена функция отображения для данного выражения Е и состояния s. Символ = обозначает равенство по определению функиии.

Оператор присваивания - это вычисление выражения плюс присваивание его значения переменной, находящейся в левой части. Сказанное можно описать следующей функцией:

Отметим, что два сравнения, выполняющиеся в двух последних строках (ij<> х и ij = х), относятся к именам, а не значениям.

После определения полной системы для заданного языка, ее можно использовать для определения смысла полных программ этого языка. Это создает основу для очень строгого способа мышления в программировании.

Денотационная семантика может использоваться для разработки языка. Операторы, описать которые с помощью денотационной семантики тpyднo, могут оказаться сложными и для понимания пользователями языка, и тогда разработчику следует подумать об альтернативной конструкции.

С одной стороны, денотационные описания очень сложны, с другой - они дают великолепный метод краткого описания языка.


2.1.4. Декларативная семантика

Декларативная семантика является существенной характеристикой языков логического программирования, в которых программы состоят из объявлений (деклараций), а не из операторов присваивания и управляющих операторов. Эти объявления в действительности являются операторами, или высказываниями, в символьной логике.

Основная концепция декларативной семантики заключается в том, что существует простой способ определения смысла каждого оператора, и он не зависит от того, как именно этот оператор используется для решения задачи. Декларативная семантика значительно проще, чем семантика императивных (применяющихся в компьютерах с фон-неймановской архитектурой) языков. Она не требует для проверки отдельного оператора рассмотрения его контекста, локальных объявлений или последовательности вьшолнения программы.

Формальное определение семантики становится общепринятой частью определения нового языка. Стандартное описание языка PL/1 включает в себя VDL-подобную нотацию, описывающую семантику операторов PL/1, а для языка Ada было разработано определение на основе денотационной семантики. Тем не менее, изучение формальных определений семантики не оказало такого сильного влияния на практическое определение языков, как изучение формальных грамматик - на определение синтаксиса. Ни один из методов определения семантики не оказался по настоящему полезным ни для пользователя, ни для разработчиков компиляторов языков программирования.


назад | содержание | вперед