Определения
Начнем с определения термина типа. За основу возмем определение термина абстрактный тип данных (АТД), данное Бертраном Мейером (Bertrand Meyer) [].
Спецификация АТД состоит из четырех разделов:
- типы;
- сигнатуры функций;
- аксиомы функций и типов;
- предусловия применения частично определенных функций.
Далее будем придерживаться следующих соглашений:
- саму спецификацию будем называть типом;
- доменом типа будем называть множество всех величин данного типа, то есть величин, удовлетворяющих спецификации;
- в разделе типы (по Мейеру) будут содержаться обозначение домена типа, аксиомы для его описания, а также, возможно, спецификации простых вспомогательных типов;
- в разделе функций будут вводиться сигнатуры функций, предусловия и постусловия применения функций; из всего набора функций выделяются функции-генераторы (generator, на выходе имеется обозначение домена типа) и функции-наблюдатели (observer, на выходе функции отсутствует обозначение домена типа); особенно важную роль играют функции, не выводимые из других функции;
- в разделе аксиом будут определяться аксиомы, описывающие попарное применение функций-генераторов и функций-наблюдателей.
В простых и привычных случаях , когда это не приводит к путанице, типом можно называть домен типа. Например, можно называть типом прямое произведение двух множеств A ? B, подразумевая, что имеется спецификация функций проекции. Обозначение A ? B, мыслимое без функций проекции – это домен типа, A ? B, мыслимое вместе с аксиомами функций проекции, – это тип.
Далее, уточним следующее определение Мейера []: Класс – это абстрактный тип данных, поставляемый с возможно частичной реализацией.
Спецификация (то есть тип), в которой произведена замена аксиом, описывающих попарное поведение функций, на частично определенные функции, будем называть аппликативной реализацией. Определение класса на языке программирования L, удовлетворяющее требованиям спецификации, будет называть (обычно, императивной) L-реализацией.
