ГОСТ I* ИСО/МЭК 10746-3-2001
Для заданной начальной цели I,
е
|—а £ [) адюрнтм состоит в применении правил вывода в обратном
порядке для получения подцелей в случаях (гее), (fun), (red), (pro) и (uni). Построенное таким образом дерево
целей называется деревом выполнении. Дерево выполнения всегда конечно: если
1
Ss —положение, которое
добавляется к £, то t и s являются переменными типов в dom(r); правила (fun), (pro), (uni) и (red) уменьшают
размер текущей цели, заменяя ее подвыражениями цели, а каждое применение (гее) увеличивает I.
Дерево выполнения успешно, если все листья соответствуют применению одного изправил (asanp), (bot),
(top) или (var). Оно неудачно, если по крайней мере один лист является неосуществимой целью (т.с. к ней не
может быть применено ни одно из правил). Если дерево выполнения, соответствующее цели 0
е
|—
а
£ р
успешно, то его обозначают (— А
а
£ ().
Для заданных рекурсивных типов а и (5. таких, что а = Val(l|t f,) и р = Val(t2, е2) (
е
,
и е
2 определены
выше), алгоритмом порождается отношение подтипа (£ А), определяемое следующим образом:
н £ А б <=> |— A t, £ t2
Эго новое отношение подтипа совпадает с предыдущим, т.с.:
- для данных а. 3 в Т, сети а £ А р, то
а
£ R р;
- для данных о, р в Т, если a £ R [), то а £ А р.
А.З Типы сигнатур интерфейсов сигналов
Формализуются путем их интерпретации на языке Туре. Множество типов сигнатур интерфейсовсигналов
обозначают Туре,,,. Элементы Туре,,, абстрактно определяются через использование двух функций: iiuypc :
Туре.,, -з Туре и outype : Турс11(; -> Туре. Дли заданного типа сигнатуры интерфейса сигналов intype описывает
множество начальных сигналов, a outype —ответных.
Элементы Туре, связанные с типом сигнатуры интерфейса сигналов функциями intype и outype, опреде
ляются строю определенными средами с общим подмножеством Туре, определяемом грамматикой рисунка А.6,
где метки a,, i е {1
.......
q) предполагаются различными. В результате рисунок А.6 предоставляет абстрактный
синтаксис для сигнатур интерфейсов сигналов. Метки а, соответствуют именам сигналов. Продукция Arg
соответствует параметрам сигнала. Продукция Sigsig соответствует отдельным сигнатурам сигналов. Функцио
нальный вид, принятый для отдельных сигнатур сигналов, подчеркивает аналогию с объявлениями сигнатур.
Отношение подтипа для типов интерфейсов сигналов (£ s) определяется следующим образом:
V X,, l2е Туре^. I, £ I, = 1,.intype £ l2.intypc Аl2.outype £ I,.outype
a ::
=
< a, : Sigsig..........aq : Sigsig>
Sigsig : : ■=
Arg —з Nil
Arg :: "
Nil 1
1
, x ... x ip
Рисунок А.6 —Абстрактный синтаксис для типов сигнатур интерфейсов сигналов
А.4 Типы сигнатур интерфейсов операций
Типы сигнатур интерфейсов операционного сервера формализуются путем их интерпретации на языке
Туре (типы сигнатур шггсрфейсов операционного клиента могут быть получены непосредственно из них как
дополнения). Множество типов интерфейсов операционного сервера обозначают Typeu(S). Элементы
Typc„(S) абстрактно определяются через использование функции optype : Type0(S) -» Type.
Элементы Туре, связанные с типом сигнатуры интерфейса операций функцией optype, определяются
строго определенными средами с общим подмножеством Туре, определяемом грамматикой рисунка А.7. где
метки a,, i е {1, . . . . q} предполагаются различными, а метки с,, i е{1, . . . . q} —различными в контексте
продукции Opsig.
< a,: Opsig
..........
д ,: Opsig>
Arg -3 Term | Arg -> Nil
| c, : Arg
-----
- cq : Atg|
а : :=
Opsig :: -
Term:: =
Arg:: -
Nil 1
1
, x ... x tp
Рисунок А.7 —Абстрактный синтаксис для типов сигнатур интерфейсов операций
В результате рисунок А.7 предоставляет абстрактный синтаксис для сигнатур интерфейсов операций.
Продукция Opsig соответствует отдельным сигнатурам операций. В частности, продукция Opsjg вида Arg -з Term
соответствует запросу; продукция Opsig вида Arg -з Nil соответствует сообщению. Продукция Arg
соответствует
so