ГОСТ Р ИСО/МЭК 10746-3-2001
Для заданной начальной цели Z, е |— а < в алгоритм состоит в применении правил вывода в обратном порядке для получения подцелей в случаях (rec), (fun), (red), (pro) и (uni). Построенное таким образом дерево целей называется деревом выполнения. Дерево выполнения всегда конечно: если t < s — положение, которое добавляется к Z, то t и s являются переменными типов в dom(e); правила (fun), (pro), (uni) и (red) уменьшают размер текущей цели, заменяя ее подвыражениями цели, а каждое применение (rec) увеличивает Z.
Дерево выполнения успешно, если все листья соответствуют применению одного из правил (assmp), (bot), (top) или (var). Оно неудачно, если по крайней мере один лист является неосуществимой целью (т.е. к ней не может быть применено ни одно из правил). Если дерево выполнения, соответствующее цели 0е |— а < в успешно, то его обозначают |— А а < в.
Для заданных рекурсивных типов а и в, таких, что а = Val(t;, е;) и в = Val(t2, е2) (е; и е2 определены выше), алгоритмом порождается отношение подтипа (< А), определяемое следующим образом:
а < А в <=> |— А t; < t2
Это новое отношение подтипа совпадает с предыдущим, т.е.:
- для данных а, в в Т, если а < А в, то а < R в;
- для данных а, в в Т, если а < R в, то а < А в.
А.З Типы сигнатур интерфейсов сигналов
Формализуются путем их интерпретации на языке Type. Множество типов сигнатур интерфейсов сигналов обозначают Typesig. Элементы Typesig абстрактно определяются через использование двух функций: intype : Typesjg ^ Type и outype : Typesig ^ Type. Для заданного типа сигнатуры интерфейса сигналов intype описывает множество начальных сигналов, а outype — ответных.
Элементы Type, связанные с типом сигнатуры интерфейса сигналов функциями intype и outype, определяются строго определенными средами с общим подмножеством Type, определяемом грамматикой рисунка А.6, где метки а;, i е {1, ... , q} предполагаются различными. В результате рисунок А.6 предоставляет абстрактный синтаксис для сигнатур интерфейсов сигналов. Метки а; соответствуют именам сигналов. Продукция Arg соответствует параметрам сигнала. Продукция Sigsig соответствует отдельным сигнатурам сигналов. Функциональный вид, принятый для отдельных сигнатур сигналов, подчеркивает аналогию с объявлениями сигнатур.
Отношение подтипа для типов интерфейсов сигналов (< s) определяется следующим образом:
V A;, I2 е Typesig, l; < I2 = l;.intype < ^.intype Л ^.outype < l;.outype
|
а : |
: = < a; : Sigsig, . . . , aq : SigsigZ |
|
Sigsig : |
= Arg ^ Nil |
|
Arg : |
= Nil | t; x . . . x tp |
Рисунок А.6 — Абстрактный синтаксис для типов сигнатур интерфейсов сигналов
А.4 Типы сигнатур интерфейсов операций
Типы сигнатур интерфейсов операционного сервера формализуются путем их интерпретации на языке Type (типы сигнатур интерфейсов операционного клиента могут быть получены непосредственно из них как дополнения). Множество типов интерфейсов операционного сервера обозначают Type0(S). Элементы Type0(S) абстрактно определяются через использование функции optype : Type0(S) ^ Type.
Элементы Type, связанные с типом сигнатуры интерфейса операций функцией optype, определяются строго определенными средами с общим подмножеством Type, определяемом грамматикой рисунка А.7, где метки а;, i е {1, . . . , q} предполагаются различными, а метки C;, i е{1, . . . , q} — различными в контексте
|
продукции Opsig. |
|
|
а : |
: = < aj : Opsig, . . . , aq : OpsigZ |
|
|
Opsig : |
= Arg ^ Term | Arg ^ Nil |
|
|
Term : |
= [ c; : Arg, . . . , Cq : Arg] |
|
|
Arg : |
: = Nil | t; x . . . x tp |
Рисунок А.7 — Абстрактный синтаксис для типов сигнатур интерфейсов операций
В результате рисунок А.7 предоставляет абстрактный синтаксис для сигнатур интерфейсов операций. Продукция Opsig соответствует отдельным сигнатурам операций. В частности, продукция Opsig вида Arg ^ Term соответствует запросу; продукция Opsig вида Arg ^ Nil соответствует сообщению. Продукция Arg соответствует
50