ГОСТ Р ИСО/МЭК 10746-3-2001
что каждая переменная типа в среде представляет тип. Свя зь между переменными типов и элементами Т в среде
можно понимагь как определяющие взаимную зависимость уравнения для соответствующих типов.
Формально, нусгьу„,
—
множество сгрого определенных сред; определим A -*fB как частичную функцию
из А в В с конечной областью; FV(«) обозначает множества свободных переменных. встречающихся в сс
= deny rviT_ f Type IVt, t *edomiyi. Г e FV(ytt)) = > t’edom(y)}
Пусть у(t |—> a, tj |—> «| ... tq (— > aq}. y\t обозначает следующую среду:
y\t - deftq |-> a,)
Типы, связанные с переменной типа t в контексте строга определенной среды у(t е dom(y)), по определению,
естьVal(t. у), где Val —функция на типах и средах, рекурсивно определенная на рисунке А.4. Таким образом, любой
элемент Туре может быть определен как Val(t, у), где у —строго определенная среда и le dom(y).
(IT. I)Val (-L,у)= -L
(IT. 2)Val (T,y)= T
(IT. 3) Val (Nil, у ) = Nil
(IT. 4)Val ( « -» p . у >™Val (« . у ) -» Val (p , у )
(IT. 5)Val « a, : a ,
.........
a„у) = < a, : Val (a, , y)
.........
an : Val <«,, . y)
>
(IT. 6) Val ( | a, :a, , . . . , a„ : aft | . у) = 1a, : Val («, , y)
-----
- ae : Val (a,, . yl|
(IT. 7) Val (a, x ... x a n , y> = Valla, . y) x ... x Val (an . y)
(IT. 8)если t * dom (y) , ro Val ( I. у ) = t
(IT. 9)если I € dom (у),
to
Val (i, y)pt . Val (y(l>, y \ t)
Рисунок Л.4 —Семантика определений типов интерфейсов
А.2.3 Алгоритм проверки типа
Осуществляется относительно определенных выше правил равенства и подтипов. В алгоритме участвуют
две строго определенные среды в, и с2, закис, что domic,) u domic,) =*0 (сравниваемые типы связаны с двумя
переменными, одна из которых в е,, другая —в
е
2). О
н
описан как множество правил вывода, включающих
е
ш
dele,ив, и множество £ вида (1, S s,, . . . . tn £ s0J, в котором записаны включении переменных,
обнаруженные в процессе выполнения алгоритма. Правило вывода соответствует логической импликации
суждений видаI, е|— «Sp. Суждение интуитивно охватываетсправедливость и £ р вконтексте I ие. Начальные
суждения {t, S s............. £ sn}должны быть такими, что (Ц, s,, ... . tn, sn>
kj
dom(i’) = 0 .
Правила вывода приведены на рисунке А.5. На этом рисунке a, р е Туре; 1, s обозначают произвольные
переменные, и обозначает переменную не из dom(e).
(assmp)t £ s e £ = >£ .£ |—t£s
(bat)£ ,
e
|- ±£ p
(top)£ ,e |—a £ T
(var)£ .f |— u £ u
(Tun)£ ,
e
|— a 2£ a, , £ , e |—pi £ p, = > £
je
|— a| -+ p, £ a, -» p.
(red). n), £ ,£ |- a, £ p, ~ > £
£
|- < a, : a, -
------
an :a n> £ < a, : p, -
------
ae : p„ >
для n £ m
(uni)V>e{l... , n), £ ,
e
|- a, £ p, - >
Z x
1- Ia, :-
------
an : an | £ | a, : p............. am:pm |
для n £ m
(pro)Vje(i
----
n). £ .£ |— (^ £ P, " > £
£
|—a, x ... x an£ p, x ...
x
pn
(rcc)£ u
{l £s| , £ |—£<t)
£ £ (S) “ > £
x
|—
t £
s
Рисунок А.5 —Правила проверки типа интерфейса
*19