элемента.

Разделитель ≪завершения≫ более универсален. В EBNF скобки { } представляют нуль или более повторений заключаемой в них строки. Поэтому конструкция {<оператор>;} представляет нуль или более операторов, завершаемых точкой с запятой.

Правило подстановки EBNF

<список операторов> ::= {<оператор>; }

эквивалентно паре правил подстановки в BNF

Характерный состав метасимволов EBNF:

‰. фигурные скобки { и } обозначают нуль и более повторений;

‰. квадратные скобки [ и ] обозначают необязательную конструкцию;

‰. вертикальная черта | обозначает выбор;

‰. скобки ( и ) обозначают группировку.

можно написать в EBNF:

<выражение> ::= <терм> {(+ | –) <терм>}

<терм> ::= <фактор> {(∗ | / ) <фактор>}

<фактор> ::= '('<выражение>')' | name | number

Синтаксические схемы.

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

ную форму их записи. Синтаксическая схема состоит из подсхем, определенных для каждого нетерминала грамматики. Терминалы заключаются в закругленные прямоугольники, нетерминалы в обычные прямоугольники.

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

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

Операционное определение языка программирования описывает выполнение про-

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

НЕ нашли? Не то? Что вы ищете?

Операционная семантика описывает смысл программы путем выполнения

ее операторов на простой машине-автомате. Изменения, происходящие в состоянии

машины при выполнении данного оператора, определяют смысл этого оператора.

Положим, что нам нужно выяснить смысл оператора for для языка програм-

мирования С. Мы представляем этот оператор с помощью некоторой программы

для виртуальной машины

Основные понятия аксиоматической семантики.

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

Итак, метод аксиоматической семантики служит для доказательства правиль-

ности программы.

Аксиома присваивания, правило консеквенции.

Эта аксиома ≪обслуживает≫, то есть позволяет ≪доказать≫ оператор присваивания.

Пусть x := E — оператор присваивания с постусловием Q. Тогда его предусловие,

определяемое по аксиоме

P = Qx→E

означает, что P вычисляется как Q, в котором все вхождения переменной x замеща-

ются на E, то есть на выражение из правой части оператора.

Аксиома записывается в виде следующей тройки:

{P = Qx→E} x := E {Q}

Повторим, что аксиоматическая семантика разрабатывается для доказательства

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

Правило консеквенции:

Общая форма правила вывода имеет вид

где утверждается, что если исходные высказывания S1, S2, …, SN истинны, то может

быть выведена истина для заключения S.

Правило консеквенции записывается в форме

где символ ⇒ обозначает ≪следует≫, а S — любой оператор программы.

Правило означает: если логическое высказывание {P} S {Q} — истина, а из ут-

верждения P ' следует утверждение P и из утверждения Q следует утверждение Q ',

то может быть выведено истинное логическое высказывание {P '} S {Q '}.

Это правило говорит, что постусловие может быть всегда ослаблено, а предусловие

может быть всегда усилено.

Правило вывода для последовательности операторов.

Пусть S1 и S2 — два смежных оператора, имеющих следующие пред - и постус-

ловия: {P1} S1 {P2}, {P2} S2 {P3}. Отметим, что постусловие первого оператора совпадает с предусловием второго. Первый оператор формирует данные для успешного старта второго оператора. Тогда правило вывода для последовательности из двух операторов принимает вид:

Для данного примера {P1} S1; S2 {P3} правило вывода предписывает аксиомати-

ческую проверку последовательности операторов S1; S2: они должны иметь общее

утверждение, иначе ограничение на переменные, — это {P2}. Мало того, предусловие

первого оператора должно стать общим предусловием последовательности, а постусловие

второго — общим постусловием.

Для запуска цепочки достаточно знать лишь требуемый

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

Правило вывода для условного оператора.

Данное правило позволяет получить семантически правильный условный оператор

с булевым условием ветвления B, оператором S1, который надо поместить в then-

ветвь, и оператором S2, который следует разместить в else-ветви.

У правильного условного оператора должна быть одна точка входа и одна точка

выхода. Это означает, что постусловие у S1 и S2 должно быть одинаковое, напри-

мер Q.

Предусловия операторов S1 и S2 описываются достаточно сложно. С одной

стороны, у них есть общая часть P, которая задает стартовые ограничения на ≪ариф-

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

истинном значении булева условия B, а оператор S2 — при его ложном значении.

Отсюда вывод: предусловия должны быть представлены как логические перемно-

жения прямого (инверсного) булева условия B (not B) и утверждения P:

.

Как видим, аксиоматическая семантика условного оператора не оставляет без

внимания ни одной детали, связанной с его компонентами.

Правило вывода для цикла с предусловием

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

Денотационная семантика. Состояние программы.

В этом подходе пытаются синтезировать определение функции, которую вычисляет

каждая программа, написанная на языке программирования. Спецификация языка

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

программной конструкцией.

Денотационная семантика — наиболее строгий метод для описания смысла

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

Здесь для каждой конструкции языка задается:

1) математический объект;

2) семантическая функция, которая отображает экземпляры конструкции в экзем-

пляры математического объекта.

Опросить состояние программы позволяет функция VARMAP (ij, S).

элементов:

S = {<i1, v1>, <i2, v2>, …, <in, vn>}

где ij — имя j-й переменной программы; vj — текущее значение этой переменной.

Положим, что в некоторой программе имеются три переменные с именами a,

b, c и значениями 1, 10 и 50 соответственно.

Как показано на рис. 7.7, для хранения этой информации можно использовать

≪двухэтажную≫ структуру из шести ячеек памяти:

I a b c

V 1 10 50

В ячейках ≪верхнего этажа≫ (это ячейки i1, i2, i3) хранят имена переменных,

а в ячейках ≪нижнего этажа≫ (это ячейки v1, v2, v3) — значения переменных.

Любой элемент v может иметь специальное значение undef, указывающее, что

связанная с ним переменная не определена. Эта функция для данного имени переменной ij и состояния S возвращает текущее значение переменной:

VARMAP (i1, S) = 1, VARMAP (i2, S) = 10, VARMAP (i3, S) = 50

Большинство семантических функций для программ и программных конструк-

Из за большого объема этот материал размещен на нескольких страницах:
1 2 3 4 5 6