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

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

Метод таблиц решений базируется на использовании таблиц следующего вида (см. табл. 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.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

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

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

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

где 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-й шаг: