JUN DEC Jan 27 2007 2008 2009 13 captures 6 Jan 05 - 27 Dec 08

Close Help

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

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

Для спецификации семантики функций используются следующие подходы: табличный, алгебраический и логический [5.1], а также графический [5.2].

Табличный подход для определения функций хорошо известен еще со средней школы. Он базируется на использовании таблиц. В программировании эти методы получили развитие в методе таблиц решений.

Алгебраический подход базируется на использовании равенств для определения функций. В этом случае для определения некоторого набора функций строится система равенств вида:

L1=R1,

. . .

Ln=Rn.

(5.1)

где Li и Ri, i=1, ... n, некоторые выражения, содержащие предопределенные операции, константы, переменные, от которых зависят определяемые функции (формальные параметры этих функций), и вхождения самих этих функций. Семантика определяемых функций извлекается в результате интерпретации этой системы равенств. Эта интерпретация может производится по-разному (базироваться на разных системах правил), что порождает разные семантики. В настоящее время активно исследуются операционная, денотационная и аксиоматическая семантики.

Третий подход, логический, базируется на использовании предикатов - функций, аргументами которых могут быть значения различных типов, а результатами которых являются логические значения (ИСТИНА и ЛОЖЬ). В этом случае набор функций может определяться с помощью системы предикатов. Заметим, что система равенств алгебраического подхода может быть задана с помощью следующей системы предикатов:

РАВНО(L1, R1),

. . . . . . .

РАВНО(Ln, Rn),

(5.2)

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

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

5.2. Метод таблиц решений.

Метод таблиц решений базируется на использовании таблиц следующего вида (см. табл. 5.1).

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

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

Переменные/условия	Ситуации(комбинации значений)
x1	a[1,1]	a[1,2]	...	a[1,m]	*
x2	a[2,1]	a[2,2]	...	a[2,m]	*
. . .	. . .
xn	a[n,1]	a[n,2]	...	a[n,m]	*
s1	u[1,1]	u[1,2]	...	u[1,m]	u[1,m+1]
s2	u[2,1]	u[2,2]	...	u[2,m]	u[1,m+1]
. . .	. . .
sk	u[k,1]	u[k,2]	...	u[k,m]	u[k,m+1]
Действия	Комбинации выполняемых действий

Табл. 5.1. Общая схема таблиц решений.

Нижняя часть таблицы решений определяет действия, которые требуется выполнить в той или иной ситуации, определяемой в верхней части таблицы решений. Она также состоит из нескольких (k) строк, каждая из которых связана с каким-либо одним конкретным действием, указанным в первом поле (столбце) этой строки. В остальных полях (столбцах) этой строки (т.е. для u[i, j], i=1, ... m+1, j=1, ... k) указывается, следует ли выполнять (u[i, j]= '+') это действие в данной ситуации или не следует (u[i, j]= '-'). Таким образом, первый столбец нижней части этой таблицы представляет собой список обозначений действий, которые могут выполняться в той или иной ситуации, определяемой этой таблицей. В каждом следующем столбце этой части указывается комбинация действий, которые следует выполнить в ситуации, определяемой в том же столбце верхней части таблицы решений. Для ряда таблиц решений эти действия могут выполняться в произвольном порядке, но для некоторых таблиц решений этот порядок может быть предопределен, например, в порядке следования соответствующих строк в нижней части этой таблицы.

Условия	Ситуации
Состояние светофора	Кр	Кр	Кр	Жел	Жел	Зел	Зел	Зел
T=Tкр	Нет	Нет	Да	*	*	*	*	*
T=Tжел	*	*	*	Нет	Да	*	*	*
T>Tзел	*	*	*	*	*	Нет	Да	Да
Появление привиле-гированной машины	Нет	Да	*	*	*	*	Нет	Да
Включить красный	-	-	-	-	-	-	+	-
Включить желтый	-	+	+	-	-	-	-	-
Включить зеленый	-	-	-	-	+	-	-	-
T:=0	-	+	+	-	+	-	+	-
T:=T+1	+	-	-	+	-	+	-	+
Освобож-дение пе-шеходной дорожки	-	-	-	+	-	-	-	-
Пропуск пешеходов	+	+	+	-	-	-	-	-
Пропуск машин	-	-	-	-	-	+	+	+
Действия	Комбинации выполняемых действий

Рис. 5.2. Таблица решений "Светофор у пешеходной дорожки".

Рассмотрим в качестве примера описание работы светофора у пешеходной дорожки. Переключение светофора в нормальных ситуациях должно производиться через фиксированное для каждого цвета число единиц времени (Tкр - для красного цвета, Tжел - для желтого, Tзел - для зеленого). У светофора имеется счетчик таких единиц. При переключении светофора в счетчике устанавливается 0. Работа светофора усложняется необходимостью пропускать привилегированные машины (на светофор о их появлении поступает специальный сигнал) с минимальной задержкой, но при обеспечении безопасности пешеходов. Приведенная на рис. 5.2 таблица решений описывает работу такого светофора и порядок движения у него в каждую единицу времени . Звездочка (*) в этой таблице означает произвольное значение соответствующего условия.

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

В операционной семантике алгебраического подхода к описанию семантики функций рассматривается следующий частный случай системы равенств (5.1):

f1(x1, x2, ... , xk)= E1,

f2(x1, x2, ... , xk)= E2,

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

fn(x1, x2, ... , xk)= En,

(5.3)

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

Операционная семантика интерпретирует эти равенства как систему подстановок. Под подстановкой

              | s            E |              | T

fi(x1, x2, ... , xk)= Ei
задает в параметрической форме множество правил подстановок вида

         | x1, x2, ... , xkfi(T1, T2, ... , Tk) -> Ei |          | T1, T2, ... , Tk

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

В качестве примера операционной семантики рассмотрим определение функции F(n)=n! Она определяется следующей системой равенств:

F(0)=1,

F(n)=F(n-1)*n.

Для вычисления значения F(3) осуществляются следующие шаги.

1-й шаг:

F(0)=1,

F(3)=F(2)*3.

2-й шаг:

F(0)=1,

F(3)=F(2)*3,

F(2)=F(1)*2.

3-й шаг:

F(0)=1,

F(3)=F(2)*3,

F(2)=F(1)*2,

F(1)=F(0)*1.

4-й шаг:

F(0)=1,

F(3)=F(2)*3,

F(2)=F(1)*2,

F(1)=1.

5-й шаг:

F(0)=1,

F(3)=F(2)*3,

F(2)=2,

F(1)=1.

6-й шаг:

F(0)=1,

F(3)=3,

F(2)=2,

F(1)=1.

Значение F(3) на 6-ом шаге получено.

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

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

Основные идеи денотационной семантики проиллюстрируем на более простом случае, когда система равенств (5.3) является системой языковых уравнений:

X1= phi[1,1] U phi[1,2] U ... U phi[1,k1],

X2= phi[2,1] U phi[2,2] U ... U phi[2,k2],

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

Xn= phi[n,1] U phi[n,2] U ... U phi[n,kn],

(5.4)

Xi=Ж

Как известно, формальный язык - это множество цепочек в некотором алфавите. Такую систему можно рассматривать как одну из интерпретаций набора правил некоторой грамматики, представленную в форме Бэкуса-Наура (каждое из приведенных уравнений является аналогом некоторой такой формулы). Пусть фиксирован некоторый алфавит A={a1, a2, ... , am} терминальных символов грамматики, из которых строятся цепочки, образующие используемые в системе (5.4) языки. Символы X1, X2, ... , Xn являются метапеременными грамматики, здесь будут рассматриваться как переменные, значениями которых являются языки (множества значений этих метапеременных). Символы phi[i,j], i=1,...,n, j=1,...,kj, обозначают цепочки в объединенном алфавите терминальных символов и метапеременных:

phi[i,j] О (A | {X1, X2, ... , Xn})* .

Цепочка phi[i,j] рассматривается как некоторое выражение, определяющее значение, являющееся языком (множеством цепочек в алфавите A). Такое выражение определяется следующим образом. Если значения X1, X2, ... , Xn заданы, то цепочка

phi= Z1 Z2 ... Zk , Zi О (A | {X1, X2, ... , Xn}),

обозначает сцепление множеств Z1, Z2, ... , Zk , причем вхождение в эту цепочку символа aj представляет множество из одного элемента {aj}. Это означает, что phi определяет множество цепочек

{p1 p2 ... pk | pj О Zj, j=1,...,k},

причем цепочка

p1 p2 ... pk

представляет собой последовательность выписанных друг за другом

цепочек p1, p2, ... , pk . Таким образом, каждая правая часть уравнений системы (5.4) представляет собой объединение множеств цепочек.

Решением системы (5.4) является набор значений (языков)

L1, L2, ... , Ln

переменных X1, X2, ... ,Xn, для которых все уравнения системы (5.4) превращаются в тождество.

Рассмотрим в качестве примера частный случай системы (5.4), состоящий из одного уравнения

X= a X U b X U c

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

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

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

L1=L U {phi a | phi О {a,b}*}

и

L2=L U {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),

. . . . . . . . . .

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

(5.5)

В качестве начального приближения решения этой системы примем набор языков (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.

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, ni0},

ПУСТ={}, ДНО - особое значение (зависящее от реализации магазина), не принадлежащее D. Тогда указанный набор аксиом определяют свойства магазина.

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

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

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

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

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

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

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

5.2. Ian Sommerville. Software Engineering. - Addison-Wesley Publishing Company, 1992. - P.

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

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