ГОСТ Р ИСО/МЭК 10746-3-2001
что каждая переменная типа в среде представляет тип. Связь между переменными типов и элементами Т в среде можно понимать как определяющие взаимную зависимость уравнения для соответствующих типов.
Формально, пусть ywf — множество строго определенных сред; определим А —■ fB как частичную функцию из А в В с конечной областью; FV(a) обозначает множество свободных переменных, встречающихся в а:
Ywf = def{y: Tvar — f Type | V t, t ’ e dom(y), t’ e FV(y(t)) = > t’e dom(y)}
Пусть у = {t |— > а, tj |— > а; ... tq — > aq}. y\t обозначает следующую среду:
y\t = def {tj |— a! . . . tq |—> aq}
Типы, связанные с переменной типа t в контексте строго определенной среды у (t e dom(y)), по определению, есть Val(t, у), где Val — функция на типах и средах, рекурсивно определенная на рисунке А.4. Таким образом, любой элемент Type может быть определен как Val(t, у), где у — строго определенная среда и t e dom(y).
|
(ГГ. 1) |
Val (T, у ) = T |
|
|
(IT. 2) |
Val (T, у ) = T |
|
|
(IT. 3) |
Val (Nil, у ) = Nil |
|
|
(IT. 4) |
Val ( а —■ в , Y ) = Val (а , у ) —■ Val (в , у ) |
|
|
(IT. 5) |
Val (< aj : аJ , . . . , an : аn > , у) = < al : Val faj , у) , . . . , an : Val (ад |
, у) > |
|
(IT. 6) |
Val ( [ aj : аJ , . . . , an : аn ] , у) = [ aj : Val (аJ , у) , . . . , an : Val (ад |
, у)] |
|
(IT. 7) |
Val ^j x . . . x ад , у) = Val ^j , у) x . . . x Val (ад , у) |
|
|
(IT. 8) |
если t g dom (у) , то Val ( t, у ) = t |
|
|
(IT. 9) |
если t e dom (у) , то Val (t, у) = pt . Val (у (t) , у \ t) |
|
Рисунок А.4 — Семантика определений типов интерфейсов
А.2.3 Алгоритм проверки типа
Осуществляется относительно определенных выше правил равенства и подтипов. В алгоритме участвуют две строго определенные среды £j и е2, такие, что dom(£j) u dom(e2) = 0 (сравниваемые типы связаны с двумя переменными, одна из которых в £j, другая — в £2). Он описан как множество правил вывода, включающих £ = def£jU£2 и множество X вида {tj < sj, . . . , tn < sn}, в котором записаны включения переменных, обнаруженные в процессе выполнения алгоритма. Правило вывода соответствует логической импликации суждений вида X, £ |— а < в. Суждение интуитивно охватывает справедливость а < в в контексте X и £. Начальные суждения {tj < sj, . . . , tn < sn} должны быть такими, что {tj, sj, ... , tn, sn} u dom(£) = 0 .
Правила вывода приведены на рисунке А.5. На этом рисунке а, в e Type; t, s обозначают произвольные переменные, и обозначает переменную не из dom(£).
|
(assmp) |
|
|
t < s e X = > X ,£ |— t < s |
|
(Lot) |
|
|
X ,£ |— T < в |
|
(top) |
|
|
X ,£ |— а < T |
|
(var) |
|
|
X , £ |— U < U |
|
(fun) |
|
X , £ | |
— а2 < аJ , X , £ | вJ < в2 > X ,£ |— aJ —— в1 < а2 —— в2 |
|
(red) |
Vje{1, .. |
, n}, X , £ |
|— а < в:' = > X ,£ |— < aj : аJ , . . . , Кд : an > < < aj : вJ , .. . , Кд : вn > для n < m |
|
(uni) |
Vje{1, . |
. , n}, X ,£ |
|— а < в] = > X ,£ | [ aj : а; , . . . , Кд : an ] < [ aj : вJ , . . . , am : вт ]
для n < m |
|
(pro) |
|
Vje{1, ... |
, n}, X ,£ |— а < в_] = > X ,£ |— а; x . . . x ад < в1 x . . . x вд |
|
(ree) |
|
|
X u {t < s} , £ |— £ (t) < £ (s) = > X ,£ |— t < s |
|
|
Рисунок А.5 — Правила проверки типа интерфейса |
49