Приложение А (обязательное). Формальные правила для вычислительных супертипов/подтипов

Приложение А
(обязательное)

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

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

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

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

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

- , , и т.д. - типы;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

- ;

- < : , . . . , : >;

- [: , . . . , : ];

- х ... х .

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

Правила подтипов дают в виде правил вывода суждений, похожих на программу в Прологе. Суждения имеют вид Г |- , где Г - множество предложений об образовании подтипа для переменных типа в виде { , ... , }. Типичное правило может иметь следующий вид:

Неформально это означает, что для того, чтобы определить, имеет ли место Г |- , следует определить, имеют ли место Г |- и Г |-. Если эти цели достигнуты, то можно сделать вывод, что является подтипом .

Рисунок A.2 - Правила равенства типов

Правила подтипов приведены на рисунке А.3. Можно сказать, что а является подтипом , если |- может быть выведено с помощью правил подтипов и правил равенства.

А.2.2 Определения типов

Элементы множества Туре определяются множеством уравнений взаимозависимости, смоделированным как строго построенная среда. Среда является конечным отображением между переменными типов и типами, относящимися к Т, где Т - нерекурсивное подмножество Туре. Строго построенная среда является такой средой, что свободные переменные типа , связанные с переменной t в области , все относятся к области . Интуитивно ясно,

Рисунок А.3 - Правила подтипов

что каждая переменная типа в среде представляет тип. Связь между переменными типов и элементами Т в среде можно понимать как определяющие взаимную зависимость уравнения для соответствующих типов.

Формально, пусть - множество строго определенных сред; определим как частичную функцию из А в В с конечной областью; FV() обозначает множество свободных переменных, встречающихся в :

Типы, связанные с переменной типа t в контексте строго определенной среды (tdom()), по определению, есть Val(t, ), где Val - функция на типах и средах, рекурсивно определенная на рисунке А.4. Таким образом, любой элемент Туре может быть определен как Val(t, ), где - строго определенная среда и t dom().

Рисунок A.4 - Семантика определений типов интерфейсов

А.2.3 Алгоритм проверки типа

Осуществляется относительно определенных выше правил равенства и подтипов. В алгоритме участвуют две строго определенные среды и , такие, что dom() dom() = (сравниваемые типы связаны с двумя переменными, одна из которых в , другая - в ). Он описан как множество правил вывода, включающих = def и множество вида {, . . . , }, в котором записаны включения переменных, обнаруженные в процессе выполнения алгоритма. Правило вывода соответствует логической импликации суждений вида , |- . Суждение интуитивно охватывает справедливость в контексте и . Начальные суждения {, ... , } должны быть такими, что {, , ... , , }dom() = .

Правила вывода приведены на рисунке А.5. На этом рисунке , Type; t, s обозначают произвольные переменные, и обозначает переменную не из dom().

Рисунок A.5 - Правила проверки типа интерфейса

Для заданной начальной цели , |- алгоритм состоит в применении правил вывода в обратном порядке для получения подцелей в случаях (rec), (fun), (rcd), (pro) и (uni). Построенное таким образом дерево целей называется деревом выполнения. Дерево выполнения всегда конечно: если ts - положение, которое добавляется к , то t и s являются переменными типов в dom(); правила (fun), (pro), (uni) и (rcd) уменьшают размер текущей цели, заменяя ее подвыражениями цели, а каждое применение (rec) увеличивает .

Дерево выполнения успешно, если все листья соответствуют применению одного из правил (assmp), (bot), (top) или (var). Оно неудачно, если по крайней мере один лист является неосуществимой целью (т.е. к ней не может быть применено ни одно из правил). Если дерево выполнения, соответствующее цели |- успешно, то его обозначают |- А .

Для заданных рекурсивных типов и , таких, что = Val(, ) и = Val(, ) ( и определены выше), алгоритмом порождается отношение подтипа (А), определяемое следующим образом:

Это новое отношение подтипа совпадает с предыдущим, т.е.:

- для данных , в Т, если , то R ;

- для данных , в Т, если R , то А .

А.3 Типы сигнатур интерфейсов сигналов

Формализуются путем их интерпретации на языке Туре. Множество типов сигнатур интерфейсов сигналов обозначают . Элементы абстрактно определяются через использование двух функций: intype : Туре и outype : Type. Для заданного типа сигнатуры интерфейса сигналов intype описывает множество начальных сигналов, a outype - ответных.

Элементы Туре, связанные с типом сигнатуры интерфейса сигналов функциями intype и outype, определяются строго определенными средами с общим подмножеством Туре, определяемом грамматикой рисунка А.6, где метки , i {1, ... , q} предполагаются различными. В результате рисунок А.6 предоставляет абстрактный синтаксис для сигнатур интерфейсов сигналов. Метки соответствуют именам сигналов. Продукция Arg соответствует параметрам сигнала. Продукция Sigsig соответствует отдельным сигнатурам сигналов. Функциональный вид, принятый для отдельных сигнатур сигналов, подчеркивает аналогию с объявлениями сигнатур.

Отношение подтипа для типов интерфейсов сигналов (s) определяется следующим образом:

Рисунок А.6 - Абстрактный синтаксис для типов сигнатур интерфейсов сигналов

А.4 Типы сигнатур интерфейсов операций

Типы сигнатур интерфейсов операционного сервера формализуются путем их интерпретации на языке Туре (типы сигнатур интерфейсов операционного клиента могут быть получены непосредственно из них как дополнения). Множество типов интерфейсов операционного сервера обозначают (S). Элементы (S) абстрактно определяются через использование функции optype : (S) Type.

Элементы Туре, связанные с типом сигнатуры интерфейса операций функцией optype, определяются строго определенными средами с общим подмножеством Туре, определяемом грамматикой рисунка А.7, где метки , i {1, . . . , q} предполагаются различными, а метки , i{1, . . . , q} - различными в контексте продукции Opsig.

Рисунок A.7 - Абстрактный синтаксис для типов сигнатур интерфейсов операций

В результате рисунок А.7 предоставляет абстрактный синтаксис для сигнатур интерфейсов операций. Продукция Opsig соответствует отдельным сигнатурам операций. В частности, продукция Opsig вида Arg Term соответствует запросу; продукция Opsig вида ArgNil соответствует сообщению. Продукция Arg соответствует параметрам вызова. Продукция Term соответствует завершению. Nil в левой части продукции Opsig означает, что данный вызов не имеет параметров. Nil в правой части продукции Opsig (т.е. в сигнатуре сообщения) означает, что завершение не ожидается. Метки соответствуют именам операций. Метки соответствуют именам завершений.

Отношение подтипа для типов интерфейсов операционного сервера (о) определяется следующим образом:

, ,

А.5 Типы интерфейсов потоков

Полное определение правил подтипов сигнатур для интерфейсов потоков находится вне сферы действия настоящей базовой модели (см. 7.2.4.2). Отметим, однако, что отдельные типы сигнатур потоков могут быть формализованы путем их интерпретации на языке Туре.

Элементы Туре, связанные с сигнатурой потока, определяются строго определенными средами с общим подмножеством Туре, определяемым грамматикой рисунка А.8, где метка соответствует имени потока.

В этом случае правила подтипов в 7.2.4.2, связанные с соответствующими потоками (при условии, что они имеют одинаковую причинность), соответствуют отношению подтипа.

Рисунок A.8 - Абстрактный синтаксис для типов сигнатур интерфейсов потоков

А.6 Пример

Рассмотрим следующие определения типа сигнатуры интерфейса операций (т.е. строго определенную среду):

и t, Tvar; op, factory, new, ok, nok L (op, factory и new - имена операций; ok и nok - имена завершений).

Интуитивно ясно, что среда соответствует определению двух типов t и . имеет только одну операцию new, которая не имеет аргументов и возвращает указатель на экземпляр типа t. Можно представить, например, что является типом производителя объектов, который по запросу (т.е. при каждом вызове операции new) создает объекты с интерфейсом типа t. t имеет две операции: ор и factory. Операция ор получает в качестве аргумента указатель на экземпляр объекта типа t - это первый пример рекурсивного определения. Операция factory не имеет аргументов и возвращает указатель на экземпляр типа . Можно представить, например, что в целях управления каждый объект с интерфейсом типа t может по запросу (т.е. при вызове операции factory) возвращать указатель на создавшего его производителя. Это второй пример рекурсивного определения, так как ссылается на t.

Применяя данное выше определение Val, определяя = def{ |- > } и используя правило равенства Е.10, получаем: