ВУЗ: Житомирский государственный университет им. Ивана Франко
Категория: Лекция
Дисциплина: Программирование
Добавлен: 18.02.2019
Просмотров: 660
Скачиваний: 9
Всё, что вообще может быть сказано, должно быть сказано ясно, а о чём невозможно говорить, о том следует молчать.
Л. Витгенштейн
Лекция 5.
МЕТОДЫ СПЕЦИФИКАЦИИ СЕМАНТИКИ
ФУНКЦИЙ
Основные подходы к спецификации семантики функций. Табличный подход, метод таблиц решений. Алгебраический подход: операционная, денотационная и аксиоматическая семантики. Языки спецификаций.
-
Основные подходы к спецификации семантики функций.
Для спецификации семантики функций используются следующие подходы: табличный, алгебраический и логический [5.1, стр.30-73], а также графический [5.2].
Табличный подход для определения функций хорошо известен ещё со средней школы. Он базируется на использовании таблиц. В программировании эти методы получили развитие в методе таблиц решений.
Алгебраический подход для определения функций базируется на использовании равенств. В этом случае для определения некоторого набора функций строится система равенств вида:
L1=R1,
. . . (5.1)
Ln=Rn.
где Li и Ri, i=1, ... n, некоторые выражения, содержащие предопределенные операции, константы, переменные, от которых зависят определяемые функции (формальные параметры этих функций), и вхождения самих этих функций. Семантика определяемых функций извлекается в результате интерпретации этой системы равенств. Эта интерпретация может осуществляться по-разному (базироваться на разных системах правил), что порождает разные семантики. В настоящее время активно исследуются операционная, денотационная и аксиоматическая семантики.
Третий подход, логический, базируется на использовании предикатов функций, у которых аргументами могут быть значения различных типов, а результатами являются логические значения (ИСТИНА и ЛОЖЬ). В этом случае набор функций может определяться с помощью системы предикатов. Заметим, что система равенств алгебраического подхода может быть задана с помощью следующей системы предикатов:
РАВНО(L1, R1),
. . . (5.2)
РАВНО(Ln, Rn),
где предикат РАВНО истинен, если равны значения первого и второго его аргументов. Это говорит о том, что логический подход располагает не меньшими возможностями для определения функций, однако он требует от разработчиков ПС умения пользоваться методами математической логики, что, к сожалению, не для всех разработчиков оказывается приемлемым. Более подробно этот подход мы рассматривать не будем.
Графический подход также известен еще со средней школы. Но в данном случае речь идет не о задании функции с помощью графика, хотя при данном уровне развития компьютерной техники ввод в компьютер таких графиков возможен и они могли бы использоваться (с относительно небольшой точностью) для задания функций. В данном случае речь идет о графическом задании различных схем, выражающих сложную функцию через другие функции, связанными с какими-либо компонентами заданной схемы. Графическая схема может определять ситуации, когда для вычисления представляемой ею функции должны применяться связанные с этой схемой более простые функции. Графическая схема может достаточно точно определять часть семантики функции. Примером такой схемы может быть схема переходов состояний конечного автомата, такая, что в каждом из этих состояний должна выполняться некоторая дополнительная функция, указанная в схеме.
5.2. Метод таблиц решений.
Метод таблиц решений базируется на использовании таблиц следующего вида (см. табл. 5.1).
-
Переменные/условия
Ситуации
(комбинации значений)
x1a[1,1]
a[1,2]
...
a[1,m]
*
x2
a[2,1]
a[2,2]
...
a[2,m]
*
. . .
. . .
xna[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. Общая схема таблиц решений.
Верхняя часть этой таблицы определяет различные ситуации, в которых требуется выполнять некоторые действия (операции). Каждая строка этой части задает ряд значений некоторой переменной или некоторого условия. Первый столбец этой части представляет собой список переменных или условий, от значений которых зависит выбор определяемых ситуаций. В каждом следующем столбце указывается комбинация значений этих переменных (условий), определяющая конкретную ситуацию. При этом последний столбец определяет ситуацию, отличную от предыдущих, т.е. для любых других комбинаций значений (будем обозначать их звёздочкой *), отличных от первых, определяется одна и та же, (m+1)-ая, ситуация. Впрочем, в некоторых таблицах решений этот столбец может отсутствовать.
Нижняя часть таблицы решений определяет действия, которые требуется выполнить в той или иной ситуации, определяемой в верхней части таблицы решений. Она также состоит из нескольких (k) строк, каждая из которых связана с каким-либо одним конкретным действием, указанным в первом поле (столбце) этой строки. В остальных полях (столбцах) этой строки (т.е. для u[i, j], i=1, ... m+1, j=1, ... k) указывается, следует ли выполнять (при u[i, j]= '+') это действие в данной ситуации или не следует (при u[i, j]= ''). Таким образом, первый столбец нижней части этой таблицы представляет собой список обозначений действий, которые могут выполняться в той или иной ситуации, определяемой этой таблицей. В каждом следующем столбце этой части указывается комбинация действий, которые следует выполнить в ситуации, определяемой в том же столбце верхней части таблицы решений. Для ряда таблиц решений эти действия могут выполняться в произвольном порядке, но для некоторых таблиц решений этот порядок может быть предопределён, например, в порядке следования строк в нижней части этой таблицы.
Рассмотрим в качестве примера описание работы светофора у пешеходной дорожки. Переключение светофора в нормальных ситуациях должно производиться через фиксированное для каждого цвета число единиц времени (Tкр для красного цвета, Tжёл для жёлтого, Tзел для зелёного). У светофора имеется счётчик таких единиц. При переключении светофора в счётчике устанавливается 0. Работа светофора усложняется необходимостью пропускать привилегированные машины (при их появлении на светофор поступает специальный сигнал) с минимальной задержкой, но при обеспечении безопасности пешеходов. Приведённая на рис. 5.2 таблица решений описывает работу такого светофора, управляющего порядком движения у него в каждую единицу времени. Звёздочка (*) в этой таблице означает произвольное значение соответствующего условия.
|
|
Ситуации |
|||||||
|
Состояние светофора |
Кр |
Кр |
Кр |
Жёл |
Жёл |
Зел |
Зел |
Зел |
|
T=Tкр |
Нет |
Нет |
Да |
* |
* |
* |
* |
* |
|
T=Tжёл |
* |
* |
* |
Нет |
Да |
* |
* |
* |
|
T>Tзел |
* |
* |
* |
* |
* |
Нет |
Да |
Да |
|
Появление привиле-гированной машины |
Нет |
Да |
* |
* |
* |
* |
Нет |
Да |
|
Включить красный |
|
|
|
|
|
|
+ |
|
|
Включить жёлтый |
|
+ |
+ |
|
|
|
|
|
|
Включить зелёный |
|
|
|
|
+ |
|
|
|
|
T:=0 |
|
+ |
+ |
|
+ |
|
+ |
|
|
T:=T+1 |
+ |
|
|
+ |
|
+ |
|
+ |
|
Освобожде- ние пеше-ходной дорожки |
|
|
|
+ |
|
|
|
|
|
Пропуск пешеходов |
+ |
+ |
+ |
|
|
|
|
|
|
Пропуск машин |
|
|
|
|
|
+ |
+ |
+ |
|
Действия |
Комбинации выполняемых действий |
|||||||
Рис. 5.2. Таблица решений "Светофор у пешеходной дорожки".
5.3. Операционная семантика.
В операционной семантике алгебраического подхода к описанию семантики функций рассматривается следующий частный случай системы равенств (5.1):
f1(x1, x2, ... , xk)= E1,
. . . . . . . . . . . . . (5.3)
fn(x1, x2, ... , xk)= En,
где в левых частях этих равенств явно указаны определяемые функции, каждая из которых зависит (для простоты) от одних и тех же параметров
x1, x2, ..., xk,
а правые части этих равенств представляют собой выражения, содержащие, вообще говоря, вхождения этих функций, т.е. определяемые функции могут быть рекурсивными. Поэтому определяемая функция может иметь дополнительные вхождения в левые части этой системы равенств с постоянными значениями некоторых параметров. Таким образом, каждый параметр xj вхождения определяемой функции fi в левую часть равенств (5.3) будем понимать либо как переменную yj, либо как константу cij, причём совокупность переменных
y1, y2, …, yk
представляет входные данные, для которых требуется вычислять определяемые функции.
Операционная семантика интерпретирует эти равенства как систему подстановок. Под подстановкой
s
E
T
выражения (терма) T в выражение E вместо символа s будем понимать переписывание выражения E с заменой каждого вхождения в него символа s на выражение T. Каждое равенство
fi(x1, x2, ... , xk)= Ei
задает в параметрической форме множество правил подстановок вида
x1,
x2, ... , xk
fi(T1, T2, ... , Tk) Ei ,
T1, T2, ... , Tk
где T1, T2, ... , Tk конкретные аргументы (значения или определяющие их выражения) данной функции. Каждое такое правило допускает замену в каком-либо выражении вхождения его левой части на её правую часть.
Интерпретация системы равенств (5.3) для получения значений определяемых функций в рамках операционной семантики производится следующим образом. Пусть задан набор входных данных (аргументов)
d1, d2, ... , dk.
На первом шаге осуществляется подстановка этих данных в левые и правые части равенств с выполнением там, где это возможно, предопределённых операций и с переписыванием получаемых в результате этого равенств. В результате этого будет сформирована исходная преобразуемая система равенств.
На каждом следующем шаге по текущей преобразуемой системы равенств производится формирование новой преобразуемой системы равенств (которая становится текущей) путем переписывания этих равенств со следующими преобразованиями.
-
Если правая часть очередного равенства является каким-либо значением, то это равенство не изменяется (это значение и является значением функции, указанной в левой части этого равенства).
-
В противном случае правая часть является выражением, содержащим вхождения каких-либо определяемых функций с теми или иными наборами аргументов. В этом случае для каждого вхождения функции в эту правую часть (с конкретным набором аргументов) просматриваются левые части преобразуемых равенств и выполняются следующие действия.
(2.1) Если для этого вхождения в текущей преобразуемой системе равенств находится совпадающая с ним левая часть некоторого равенства, то проверяется правая часть этого равенства
(2.1.1) и в случае, если она является уже вычисленным значением, производится подстановка этого значения вместо указанного вхождения определяемой функции,
(2.1.2) если же эта правая часть не является вычисленным значением, то указанное вхождение переписывается в неизменном виде.
(2.2) В том же случае, если для указанного вхождения в текущей преобразуемой системе равенств не находится совпадающей с ним левой части никакого равенства, то к новой преобразуемой системе равенств дописывается новое равенство. Это равенство получается из исходного равенства для определяемой функции
fi(y1, y2, …, yk),
вхождение которой в данный момент исследуется, путем подстановки аргументов этой функции из исследуемого вхождения вместо параметров y1, y2, …, yk этой функции (с выполнением предопределённых операций там, где это возможно).
Эти шаги будут осуществляться до тех пор, пока все определяемые функции не будут иметь вычисленные значения.
В качестве примера операционной семантики рассмотрим определение функции 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] phi[1,2] ... phi[1,k1],
X2= phi[2,1] phi[2,2] ... phi[2,k2],
. . . . . . . . . . . . . . . . . . . . . . . . . . . . (5.4)
Xn= phi[n,1] phi[n,2] ... phi[n,kn],
причём i-ое уравнение при ki=0 имеет вид
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] рассматривается как некоторое выражение, определяющее значение, являющееся языком. Такое выражение определяется следующим образом. Если значения X1, X2, ... , Xn заданы, то цепочка
phi= Z1 Z2 ... Zk , Zi (A {X1, X2, ... , Xn}) для i=1, ... , k,
обозначает сцепление множеств 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),
если все уравнения системы (5.4) превращаются в тождество при X1= L1, X2= L2, ... , Xn= Ln.
Рассмотрим в качестве примера частный случай системы (5.4), состоящий из одного уравнения
X= a X b X X c