Программирование (стр. 8 из 25)
Табл. 2. Таблица решений «Светофор у пешеходной дорожки».
| Условия | Ситуации | |||||||
| Состояние светофора | | | | | | | | |
| T = Tкр | Нет | Нет | Да | * | * | * | * | * |
| T = Tжёл | * | * | * | Нет | Да | * | * | * |
| T > Tзел | * | * | * | * | * | Нет | Да | Да |
| Появление привилегированной машины | Нет | Да | * | * | * | * | Нет | Да |
| Включить | – | – | – | – | – | – | + | – |
| Включить | – | + | + | – | – | – | – | – |
| Включить | – | – | – | – | + | – | – | – |
| T := 0 | – | + | + | – | + | – | + | – |
| T := T+1 | + | – | – | + | – | + | – | + |
| Освобождение пешеходной дорожки | – | – | – | + | – | – | – | – |
| Пропуск пешеходов | + | + | + | – | – | – | – | – |
| Пропуск машин | – | – | – | – | – | + | + | + |
| Действия | Комбинации выполняемых действий | |||||||
Рассмотрим в качестве примера описание работы светофора у пешеходной дорожки. Переключение светофора в нормальных ситуациях должно производиться через фиксированное для каждого цвета число единиц времени (Tкр — для красного цвета, Tжёл — для жёлтого, Tзел — для зелёного). У светофора имеется счетчик таких единиц. При переключении светофора в счетчике устанавливается 0. Работа светофора усложняется необходимостью пропускать привилегированные машины (об их появлении на светофор поступает специальный сигнал) с минимальной задержкой, но при обеспечении безопасности пешеходов. Приведенная на Табл. 2 таблица решений описывает работу такого светофора и порядок движения у него в каждую единицу времени. Звездочка (*) в этой таблице означает произвольное значение соответствующего условия.
3. Операционная семантика
В операционной семантике алгебраического подхода к описанию семантики функций рассматривается следующий частный случай системы равенств (1):
f1(x1, x2, ..., xk) = E1,f2(x1, x2, ..., xk) = E2,
(3) .........……………
fn(x1, x2, ... , xk) = En,
где в левых частях равенств явно указаны определяемые функции с формальными параметрами, включающими (для простоты) обозначения всех входных данных x1, x2, ..., xk, а правые части представляют собой выражения, содержащие, вообще говоря, вхождения этих функций с аргументами, задаваемыми некоторыми выражениями, зависящими от входных данных x1, x2, ..., 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 — конкретные аргументы (значения или определяющие их выражения) данной функции. Это правило допускает замену вхождения левой его части в какое-либо выражение на его правую часть.
Интерпретация системы равенств (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-ом шаге получено.
4. Денотационная семантика
В денотационной семантике алгебраического подхода рассматривается также система равенств вида (3), которая интерпретируется как система функциональных уравнений, а определяемые функции являются некоторым решением этой системы. В классической математике изучению функциональных уравнений (в частности, интегральных уравнений) уделяется большое внимание и связано с построением достаточно глубокого математического аппарата. Применительно к программированию этими вопросами серьезно занимался Д. Скотт [3].
Основные идеи денотационной семантики проиллюстрируем на более простом случае, когда система равенств (5.3) является системой языковых уравнений:
X1 = φ1,1 φ1,2 ... φ1,k1,X2 = φ2,1 φ2,2 ... φ2,k2,
(4) .....…………………………
Xn= φn,1 φn,2 ... φn,kn,
причем i-ое уравнение при ki = 0 имеет вид
Xi =
Как известно, формальный язык — это множество цепочек в некотором алфавите. Такую систему можно рассматривать как одну из интерпретаций набора правил некоторой грамматики, представленную в форме Бэкуса-Наура (каждое из приведенных уравнений является аналогом некоторой такой формулы). Пусть фиксирован некоторый алфавит A = {a1, a2, …, am} терминальных символов грамматики, из которых строятся цепочки, образующие используемые в системе (4) языки. Символы X1, X2, ..., Xn являются метапеременными грамматики, здесь будут рассматриваться как переменные, значениями которых являются языки (множества значений этих метапеременных). Символы φi,j, i = 1, ..., n, j = 1, ..., kj, обозначают цепочки в объединенном алфавите терминальных символов и метапеременных: