ГОСТ Р ИСО/МЭК 10746-3-2001

ПРИЛОЖЕНИЕ А (обязательное)

Формальные правила для вычислительных супертипов/подтипов

В настоящем приложении определены формальные правила образования подтипов для сигнатур вычислительных интерфейсов. Типы сигнатур вычислительных интерфейсов могут быть более высоких порядков, как подразумевается 7.2.2.4 в правилах для параметров. В приложении формализовано только подмножество первого порядка правил подтипов. Формализация характеристик более высоких порядков для типов сигнатур вычислительных интерфейсов оставлена для последующего исследования.

В настоящем приложении определена система типов первого порядка, которая состоит из языка простых типов, правил равенства типов и правил подтипов сигнатур. Здесь же описан алгоритм исследования и проверки полноты типа для системы типов. На языке типов определены типы сигнатур интерфейсов сигналов, операций и потоков. Так как образование подтипов для сигнатур интерфейсов потоков определено в 7.2.4.2 лишь частично, то данное приложение формализует только правило подтипов, которое применяется для соответствующих потоков.

А.1 Обозначения и соглашения

В настоящем приложении используют следующие обозначения:

-    а, в, у и т.д. — типы;

-    t, s и т.д. — идентификаторы для типов (т.е. переменные типов) и основные типы (т.е. постоянные типов); множество переменных (и постоянных) типов обозначают T_var;

-    а, Ь, с, aj, а₂, а_п и т.д. — идентификаторы или метки для элементов структур в языке типов; множество меток обозначают Л;

-    а [p/t] — подстановка в для t в а;

-    Nil — предопределенный постоянный тип.

А.2 Система типов

Система типов содержит постоянные типов, функции, декартовы произведения, записи, рекурсивные определения целевых объединений. Язык типов Type задается грамматикой рисунка А.1.

1

Т

| а ^ p |    а₁ х . . . х а_п

I    < ^ai : а1 , . .. , ап : ап >

I ^{[ c}i ^: Yi ^, . . . ^, Сп ^: Yn ^]

I    pt • а

Рисунок А.1 — Абстрактный синтаксис для деклараций типов

Основные типы обозначают Т (верхний) и 1 (нижний). Они играют роли, соответственно, наибольшего и наименьшего элементов в отношении подтипов. Функцию обозначают а ^ р. Декартово произведение обозначают а1 х . . . х а_п. Объединение обозначают [cj : Yi ,    . . . , с_п : Y_n    ]. Запись обозначают < aj    :    а1,    . . .    , а_п    :    а_п    >.

p является оператором связывания переменных. Рекурсивные типы могут строиться путем связывания типов с идентификаторами и ссылки на идентификатор для одного типа из другого.

В случае необходимости могут использоваться скобки для установления старшинства. При их отсутствии знак ^ присоединяется направо, а область действия p простирается направо, насколько это возможно.

Множество свободных переменных, встречающихся в а, обозначают как FV (а).

А.2.1 Правила типов

В настоящем разделе даны правила равенства типов и правила подтипов во введенном языке.

Тип а является заключенным в переменной типа t (обозначают t i а), если либо t не встречается свободным в а, либо а может быть развернут как тип одного из следующих видов:

-    а1 ^ а2;

^-    < ^а1 ^{: а}1, . . . , ^am ^{: а}Ш >;

^{-    [с}1 ^: Yl^, . . . ^{, с}п ^: Yn^];

-    а₁ х . . . х а_п.

Правила равенства типов даны на рисунке А.2. Равенство типов обозначают =.

47