ГОСТ I* ИСО/МЭК 10746-3-2001
Правила подтипов дают в виде правил вывода суждений, похожих на программу в Прологе. Суждения
имеют вид Г |—и
<.
р. где Г —множество предложений об образовании подтипа для переменных типа в виде {t,
S S,. ... . t„ £ sn}. Типичное правило может иметь следующий вид:
Г |— а,£р,, Г |— a2 S p , = > r | - a S ( i .
Неформально это означает, чтодля того, чтобы определить, имеетли место Гa £ р. следует определить,
имеют ли место Г (— a t £ р, и Г (— a 2£ р<. Если эти цели достигнуты, то можно сделать вывод, что а является
подтипом р.
Правила подтипов приведены на рисунке А.З. Можно сказать, что « является подтипом р. если 0 (—a £ р
может быть выведено с помощью правил подтипов и правил равенства.
А.2.2 Определения типов
Элементы множества Туре определяются множеством уравнений взаимозависимости, смоделированным как
строго построенная среда. Среда является конечным отображением между переменными типов и типами, относя
щимися к Т, где Т —нерекурсивное подмножество Туре. Строю построенная среда у яатястся такой средой, что
свободные переменные типа ос, связанные с переменной I в области у. все относятся кобласти у. Ин гуитивно ясно.
48
Рисунок А.З —Правила подтипов