с алфавитом A={a, b, c}. Решением этого уравнения является язык

L={ phi c | phi  {a, b}*}.

Система (5.4) может иметь несколько решений. Так в рассмотренном примере помимо L решениями являются также

L1=L  {phi a | phi  {a, b}*}

и

L2=L  {phi b | phi  {a, b}*}.

В соответствии с денотационной семантикой в качестве определяемого решения системы (5.4) принимается наименьшее решение. Решение

(L1, L2, ... , Ln)

системы (5.4) называется наименьшим, если для любого другого решения

(L1', L2',..., Ln')

выполняются соотношения

L1  L1', L2 L2', ... , Ln Ln'.

Так в рассмотренном примере наименьшим (а значит, определяемым денотационной семантикой) является решение L.

В качестве метода решения систем уравнений (5.3) и (5.4) можно использовать метод последовательных приближений. Сущность этого метода для системы (5.4) заключается в следующем. Обозначим правые части уравнений системы (5.4) операторами

Ti(X1, X2, ... , Xn).

Тогда система (5.4) примет вид

X1=T1(X1, X2, ... , Xn),

X2=T2(X1, X2, ... , Xn),

. . . . . . . . . . . (5.5)

Xn=Tn(X1, X2, ... , Xn).

В качестве начального приближения решения этой системы принимается набор языков

(L1[0], ... , Ln[0]) = (,,...,).

Каждое следующее приближение будет определяться по формуле:

(L1[i],...,Ln[i])= (T1(L1[i-1], ... , Ln[i-1]),

. . . . . . . . . . . . .

Tn(L1[i-1], ... , Ln[i-1])).

Так как операции объединения и сцепления множеств являются монотонными функциями относительно отношения порядка , то этот процесс сходится к решению

(L1, ... , Ln)

системы (5.5), т.е.

(L1, ... , Ln)= (T1(L1, ... , Ln), ... , Tn(L1, ... , Ln))

и это решение является наименьшим. Это решение называют еще наименьшей неподвижной точкой системы операторов T1, T2, ... , Tn.

В рассмотренном примере этот процесс даёт следующую последовательность приближений:

L[0]= ,

L[1]= {c}, L[2]= {c, ac, bc},

L[3]= {c, ac, bc, aac, abc, bac, bbc},

. . . . . . . . . . . . . . . .

Этот процесс сходится к указанному выше наименьшему решению L.

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

X::= X

тогда как уравнение вида

X= X

имеет вполне корректную интерпретацию в денотационной семантике.

5.5. Аксиоматическая семантика.

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

Для интерпретации системы (5.1) вводится понятие аксиоматического описания (S, E)  логически связанной пары понятий: S  сигнатура используемых в системе (5.1) символов функций f1, f2, ... , fm и символов констант (нульместных функциональных символов) c1,c2, ... , cl, а E  набор аксиом, представленный системой (5.1). Предполагается, что каждая переменная xi, i=1, ... , k, и каждая константа ci, i=1, ... , l, используемая в E, принадлежит к какому-либо из типов данных t1, t2, ... , tr, а каждый символ fi, i=1, ... , m, представляет функцию, типа

---

ti1 * ti2 * ... * tik  ti0.

Такое аксиоматическое описание получит конкретную интерпретацию, если будут заданы конкретные типы данных ti=ti', i=1, ... , r, и конкретные значения констант ci=ci', i=1, ... , l. В таком случае говорят, что задана одна конкретная интерпретация A символов сигнатуры S, называемая алгебраической системой

A=(t1', ... , tr', f1', ... , fm', c1', ... , cl'),

где fi', i=1, ... , m, конкретная функция, представляющая символ fi. Таким образом, аксиоматическое описание (S, E) определяет класс алгебраических систем (частный случай: одну алгебраическую систему), удовлетворяющих системе аксиом E, т.е. превращающих в тождества равенства системы E после подстановки в них fi', i=1, ... , m, и ci', i=1, ... , l, вместо fi и ci соответственно.

В программировании в качестве алгебраической системы можно рассматривать, например, тип данных, при этом определяемые функции представляют операции, применимые к данным этого типа. Так К. Хоор построил аксиоматическое определение набора типов данных [5.4], которые потом Н. Вирт использовал при создании языка Паскаль.

В качестве примера рассмотрим систему равенств

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

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

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

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

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

ДНО  D1, а функциональные символы представляют функции следующих типов:

УДАЛИТЬ: M  M,

ДОБАВИТЬ: M * D  M,

ВЕРХ: M  D1.

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

С помощью этого аксиоматического описания определим абстрактный тип данных, называемый магазином. Для этого зададим следующую интерпретацию символов её сигнатуры: пусть D  множество значений, которые могут быть элементами магазина, D1=D  {ДНО}, а M  множество состояний магазина, M={d1, d2, ... , dn | di  D, i=1, ... , n, n0}, ПУСТ={}, ДНО  особое значение (зависящее от реализации магазина), не принадлежащее D. Тогда указанный набор аксиом определяет свойства магазина.

С аксиоматической семантикой связана логика равенств (эквациональная логика), изучаемая в курсе "Математическая логика". Эта логика содержит правила вывода из заданного набора аксиом других формул.

5.6. Языки спецификаций.

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

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

---

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

Упражнения к Лекции 5.

5.1. Функции

function F(x, y: integer): integer;

function G(x, y: integer): integer;

function R(x, y: integer): integer;

определены с помощью операционной семантики равенствами:

R(x, y) = x*(y – 1),

F(x, y) = R(x + 1, y) - R(x, y - 1),

G(x, y) = F(x, R(x, y)).

Найти значения G(3, 3).

5.2. Функции

function F(n: integer): integer;

function G(n: integer): integer;

определены с помощью операционной семантики равенствами:

F(0)=1,

G(0)=2,

F(n)=G(n-1),

G(n)=F(n-1) + G(n-1).

Найти значения F(3) и G(3).

5.3. Формальные языки E и T определены над алфавитом

{'a', '*', '&', '<', '>'}

с помощью денотационной семантики равенствами

E= T  '*' T  E '&' T,

T= 'a'  'a*'  '<' E '>'

Какие из следующих строк

'*a&*a*&a*' ,

'*a&<a&a*>',

'*<*a*&a>&<*a*>*'

принадлежат языку E и какие из них не принадлежат языку E.

5.4. Тип R определён с помощью следующей аксиоматической семантики.

Описания:

type R= record P1, P2, P3: CHAR end;

function READ(S: R): CHAR; {READ: R  CHAR}

function SHIFT(S: R): R; {SHIFT: R  R}

function ADD(S: R, C: CHAR): R; {ADD: R * CHAR  R}

function REMOVE(S: R): R; {REMOVE: R  R}

var X, Y, Z: CHAR;

U: R;

Аксиомы:

SHIFT(ADD(ADD(ADD(U, X), Y), Z)) =

ADD(ADD(ADD(U,Y), Z), X);

REMOVE(U) = SHIFT(ADD(U, '#'));

READ(SHIFT(ADD(U, X))) = X;

Найти значение:

READ(SHIFT(SHIFT(REMOVE(ADD(ADD(U, 'a'), 'b'))))) =

Литература к Лекции 5.

1. В.Н. Агафонов. Спецификация программ: понятийные средства и их организация.  Новосибирск: Наука (Сибирское отделение), 1987.

2. Ian Sommerville. Software Engineering.  Addison-Wesley Publishing Company, 1992.

3. Д. Скотт. Теория решеток, типы данных и семантика / Данные в языках программирования.  М.: Мир, 1982.  С. 25-53.

4. К. Хоор. О структурной организации данных / У. Дал, Э. Дейкстра, К. Хоор. Структурное программирование.  М.: Мир, 1975. 

С. 98-197.

---

---

Смотрите также файлы

• Лекция 6. АРХИТЕКТУРА ПРОГРАММНОГО СРЕДСТВА.doc

• Лекция 7. РАЗРАБОТКА СТРУКТУРЫ ПРОГРАММЫ И МОДУЛЬНОЕ ПРОГРАММИРОВАНИЕ.doc

• Лекция 8. РАЗРАБОТКА ПРОГРАММНОГО МОДУЛЯ.doc

• Лекция 9. ДОКАЗАТЕЛЬСТВО СВОЙСТВ ПРОГРАММ.doc

• Лекция 10. Тестирование и отладка программного средства.doc