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

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

2) Сопоставьте понятия «абстрактный тип данных», «теория», «модель теории».

4.6. Иерархические модели типов данных

В основе теории типов лежат две идеи – типизация универсума и типизация языка. Смысл первой в том, что интуитивно обозримый универсум (пространство значений) должен строиться обозримыми шагами, исходя из (одного или нескольких) базисных типов (классов) объектов, и на каждом шаге построения строительным материалом для новых типов служат типы, полученные на предыдущих шагах. Суть второй идеи в том, что эта иерархия типов должна явно выражаться в языке, на котором формулируются утверждения рассматриваемой теории. Эти идеи интенсивно используются при построении программ средствами типизированных языков программирования: каждый новый тип данных в программах строится на основе некоторой совокупности существующих.

Иерархический тип данных строится на основе одного или нескольких примитивных типов, которые в свою очередь могут быть иерархическими. Каждый примитивный тип может быть проанализирован и реализован отдельно, без использования информации о тех типах, для построения которых он потребуется. С другой стороны, и вновь созданный тип может рассматриваться как «черный ящик», поведение которого оценивается в терминах примитивных типов. Очень полезное правило: тип данных «не знает» где он будет использован.

Рассуждая о типах данных, необходимо различать понятие типа данных как отдельного индивидуума и понятие системы типов данных программы или языка программирования. Дело в том, что рассматривая алгебры типов данных, мы по существу всегда имеем дело с несколькими типами данных, которые можно выстроить в некоторую иерархию. Например, в отмеченной ранее алгебре множеств натуральных чисел явно выделяются типы bool, nat и setofnat с одноименными основами и соответствующими множествами операций. При этом алгебра nat получается расширением алгебры типа bool, а алгебра setofnat – расширением nat. Если теперь при наличии алгебры setofnat мы хотим построить типы integer и setofinteger, то должны взять ее редукт на алгебры bool и nat и расширить его до алгебр integer и setofinteger. В результате получится алгебра, изображенная на рис.2.1.

Иерархическая модель построения системы типов данных

Рис. 4.1

На рис. 1.1 узлы обозначают типы данных, а стрелки – последовательность их построения. Система построенных типов образует алгебру setnatint. Последовательное отбрасывание узлов, из которых не выходит ни одной стрелки, позволяет получить различные ее редукты. Приведенные рассуждения дают основу для более формального сопоставления понятия типа данных с алгебраическими понятиями.

Определение 1.6. Тип данных - это либо одноосновная алгебра, либо такое приращение Т, преобразующее  - алгебру А в  - алгебру А, которое состоит ровно из одной основы, называемой конструируемой основой, и непустого множества операций, в индексах каждой из которых имя конструируемой основы встречается хотя бы один раз. Расширенную алгебру А, полученную при конструировании типа Т, будем называть алгеброй типа Т.

Определение 1.7. Сигнатура типа данных - это либо сигнатура одноосновной алгебры, либо такое приращение _Т преобразующее сигнатуру  в сигнатуру , которое состоит ровно из одного имени конструируемой основы и непустого множества знаков операций, в индексах каждого из которых это имя основы встречается хотя бы один раз.

Определение 1.8. Спецификация типа данных, или абстрактный тип данных - это сигнатура типа данных и множество аксиом, в каждой из которых хотя бы один раз встречается знак операции из данной сигнатуры. Другими словами, спецификация типа данных - это приращение теории, подчиняющееся определенным ограничениям. Расширенную теорию, полученную при конструировании спецификации типа Т, будем называть теорией типа Т.

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

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

• открытой пользователю спецификации типа;

• скрытой от пользователя реализации типа (т.е. соответствующего приращения алгебры).

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

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

тип bool =

операции: {true, false :  bool;

not : bool  bool;

or, and : bool, bool  bool};

аксиомы {true  false;

not(true) = false;

not(false) = true;

 p : bool and(false, p) = false;

and(true, p) = p;

or(false, p) = p;

or(true, p) = true}.

Моделями данного абстрактного типа данных (т.е. данной теории одноосновных алгебр) могут быть любые одноосновные алгебры, носители которых содержат два различных элемента, образуемые операциями false и true.

тип nat =

примитивный bool;

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

succ : nat nat;

,  : nat, nat bool};

аксиомы {  m, n : nat zero  n = true;

succ(m)  zero = false;

succ(m)  zero;

succ(m)  succ(n) = m  n;

m  n = and(m  n, n  m)}.

Как видно из спецификации, данный абстрактный тип расширяет теорию одноосновных алгебр bool до теории двухосновных алгебр, скажем boolnat. Нетрудно убедиться, что множество значений типа nat может представлять собой как бесконечное множество вида {0, 1, 2, … }, так и любое конечное множество вида {0, 1, 2, … n}.

тип setofnat =

примитивные {bool, nat};

операции { empty :  setofnat;

insert : setofnat, nat setofnat;

has : setofnat, nat bool};

аксиомы { x, y : nat,  s : setofnat

has(empty, x) =false;

has(insert(s, x), y) = or(x  y, has(s, y)) }.

Абстрактный тип setofnat расширяет теорию boolnat до теории, скажем, boolnatset. Алгебры, соответствующие этой теории, могут строиться расширением алгебр теории boolnat.

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