Контрольные вопросы

1) Что такое «иерархический тип данных»?

2) Чем отличается иерархический тип данных от примитивного?

3) Опишите свойства примитивного типа данных.

4) Расскажите своими словами, как строится иерархический тип данных.

5) Что представляет собой спецификация типа данных?

4.7. Типы и подтипы

Предположим, что имеются два типа Т и П и две функции into : Т  П и out : П  Т с таким свойством, что  х : П имеет место into(out(x)) = x. В этом случае говорят, что тип П является подтипом типа Т, а тип Т – образующим типом. Термин «подтип» означает, что область значений функции out представляет собой подмножество множества значений образующего типа и соответственно функция into определена только на этом подмножестве (множество значений подтипа является подмножеством значений образующего типа).

В общем случае типы Т и П могут иметь собственные множества операций. Однако поскольку каждое значение подтипа может быть преобразовано в значение образующего типа и затем обработано посредством его операций, на практике подтипы обычно рассматриваются лишь как средство наложения ограничений на множество значений образующего типа. По этой причине мы будем считать, что при определении подтипа задаются только операции into и out. Аксиомы подтипа, очевидно, в таком случае специфицируют области определения и значения этих функций.

В качестве примера рассмотрим образование подтипа oneten, выделяющего в типе nat отрезок значений от 1 до 10. Соответствующее расширение теории типа nat будет выглядеть следующим образом:

тип oneten =

примитивные nat

операции {into : nat  oneten;

out : oneten  nat};

аксиомы {  x : oneten into(out(x)) = x,

out(x)  10  out(x)  1 = true}.

Первая из аксиом показывает, что речь идет об образовании подтипа, а вторая задает область определения функции into, т.е. критерий выделения значений типа для образования подтипа. Поскольку каждый подтип обладает ровно двумя операциями into и out с очевидными типами аргументов, их явное указание становится излишним, излишне также указание первой аксиомы, свойственной все подтипам, и поэтому можно записать коротко: подтип oneten = nat(x : nat, 1  x  10).

Употребления значения подтипа в контекстах, в которых требуется значение образующего типа, всегда означает неявное использование операции out, а употребление значения образующего типа в контекстах, в которых требуется значение подтипа, всегда означает неявное использование операции into.

Контрольные вопросы

1) Сформулируйте понятие «подтип данных».

2) Какие аксиомы являются обязательными при определении подтипа данных?

3) Почему определение подтипа можно записать в краткой форме?

4.8. Типы типов

Формализация способа построения типов данных приводит к тому, что каждый тип может рассматриваться как отдельный объект, создаваемый специальной операцией конструирования типов. Это, в свою очередь, позволяет говорить о множестве типов, создаваемых указанной операцией, и тем самым – о типе всех типов данных тип.

Так же как и в отношении других типов данных, в типе данных тип можно выделить по тем или иным критериям различные подтипы. Каждый подтип типов, или ограниченный тип типов, определяет множество типов данных, обладающих каким-либо общим свойством. Распространенный класс подтипов типов составляют такие подтипы, каждый из которых накладывает условие, что тип данных, входящий в его подмножество, должен содержать среди своих операций указанный список операций. Примерами могут быть подмножество типов данных, обладающих операциями сравнения на равенство; подмножество типов данных, обладающих операциями сложения и вычитания и т.д. Тип данных может иметь и другие операции, благодаря которым он может быть отнесен к другим классам.

Если  - некоторая спецификация операций типа данных, то будем обозначать тип() множество типов данных, каждый из которых содержит в своей спецификации операции и аксиомы из . Чем уже , тем мощнее тип(). В предельном случае, когда  пусто, имеет место тип( ) = тип, т.е. охватывается все множество типов (никаких ограничений). Если считать, что тип данных тип в своем множестве операций содержит операцию spec, выделяющую у данного типа его спецификацию, то согласно общему определению подтипа (см. разд. 2.7) спецификация подтипа типов данных тип() должна иметь следующий вид:

тип тип() =

примитивные тип

операции {into : тип  тип();

out : тип()  тип};

аксиомы {  x : тип() into(out(x)) = x,

  spec(out(x)) = true}.

Однако, как и в случае подтипов «обыкновенных» типов данных, для подтипов типов также употребление операций into(x), out(x) и аксиомы into(out(x)) = x подразумеваются неявно, а в определение подтипа подставляется лишь критерий выделения значений. Тогда краткая запись предыдущего определения будет иметь вид:

подтип тип() = тип(х : тип()   spec(out(x)) = true).

Рассмотрим теперь пример определения подтипа:

подтип типсравно = тип(операции  : типсравно , типсравно  bool

аксиомы  x, y, z : типсравно

x  x = true;

x  y = y  x;

and(x  y, (y  z)) = (x  z)).

Согласно определению подтипа типов тип() каждый тип со спецификацией _k принадлежит (вернее может быть преобразован к) подтипу типов тип(_k) и каждому тип(_l), если _l  _k .