ГОСТ I* ИСО/МЭК 10746-3-2001
ПРИЛОЖЕНИЕА
(обязательное)
Формальные правила для вычислительных супергипов/иодгипов
В настоящем приложении определены формальные правила образования подтипов для сигнатур вычисли
тельных интерфейсов. Типы сигнатур вычислительмых интерфейсов могут быть более высоких порядков, как
подразумевается 7.2.2.4 в правилах для параметров. В приложении формализовано только подмножество первого
порядка правил подтипов. Формализация характеристик более высоких порядковдля типов сигнатур вычислитель ных
интерфейсов оставлена для последующего исследовании.
В настоящем приложении определена система типов первого порядка, которая состоит из языка простых
типов, правил равенства типов и правил подтиповсигнатур. Здесьже описан алгоритм исследования и проверки
полноты типа для системы типов. На языке типов определены типы сигнатур интерфейсов сигналов, операций и
потоков. Так как образование подтипов для сигнатур интерфейсов потоков определена в 7.2.4.2 лишь
частично. тх>данное приложение формализует только правило подтипов, которое применяется для соответст
вующих потоков.
А.1 Обозначения и соглашения
В настоящем приложении используют следующие обозначения:
- а, |3, у и тд. —типы;
- I. s и т.д. —идентификаторы для типов (т.с. переменные типов) и основные типы (т.е. постоянные
типов): множество переменных (и постоянных) типов обозначают TV4t;
- а, Ь. с, а,, а2, а,, и тд. —идентификаторы или метки для элементовструктур в языке типов; множество
меток обозначают Л;
-
a
|p/t| —подстановка р для t в
а:
- Nil —предопределенный постоянный тип.
А.2 Система типов
Система типов содержит постоянные типов, функции, декартовы произведении, записи, рекурсивные
определения целевых объединений. Язык типов Туре задастся грамматикой рисунка А.1.
а : : -
1
т
а -»р
а, х ... х а„
<: “
.........
..
^ :«п >
| с, :у, , . . . , с. :у„ |
ц( ■а
Рисунок А.1 —Абстрактный синтаксис для деклараций типов
Основные типы обозначают Т(верхний) и
±
(нижний). Они играют роли, соответственно, наибольшего и
наименьшего элементов в отношении подтипов. Функцию обозначаю!
а
-»р.Декартово произведение обозначают а,
х ... х а,,. Объединение обозначают |с, : у, , . . . , с„ : уп |. ’Запись обозначают < а, : а ,,. .. . а„ : <хп >.
ц является оператором связывания переменных. Рекурсивные типы могут строиться путем связывания
типов с идентификаторами и ссылки на идентификатор дтя одного типа из другого.
Вслучае необходимости могут использоваться скобки для установления старшинства. При их отсутствии
знак
—у
присоединяется направо, а область действия ц простирается направо, насколько это возможно.
Множество свободных переменных, встречающихся в а, обозначают как FV (а).
Л.2.1 Правила типов
В настоящем разделе даны правила равенства типов и правила подтипов во введенном языке.
Тип « является заключенным в переменной типа t (обозначают t 1 а), если либо i нс встречается
свободным в а. либо а может быть развернут как тип одного из следующих видов:
- «, -» «2:
- < а, : о ,,------а,„
- |С| :У,
.........
св : Ti.Il
- «1 * •• - * «в-
Правила равенства типов даны на рисунке А.2. Равенство типов обозначаю!" ».