package pointl is

function makepoint [x:Real7 у:Real) return Point;

function x coord (P:Point) return Real;

function y coord (P:Point) return Real; end pointl;

Определение пакета это не определение типа , но частично определение значения.Чтобы завершить определение значений в Ада , мы должны представить тело пакета в следующей форме:

package body ooinM is

function makepoint (x:Real, у:Real) return Point;

-implementation of makepoint function x coord (P:Pointj return Real;

-implementation of x coord function y coord (P:Pointj return Real;

-implementation of y coord end poind;

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

Ада не позволяте ,чтобы пакеты имели типы , и напрямую определяет тело функции для каждого типа функции в теле пакета.

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

Package body localpoint is

Point :Point ; -- разделяемая глобальная переменная функций marketpoint , xcoord ,y coord

procedure makepointfx,y: Real);... function x coord return Real;... function y coord return Real;... end localooint;

Скрытые локальные переменные могут быть реализованы в нашей нотации при помощи конструкции let.

value localpoint =

letp: Point = ref((0,0))

in {makepoint = fun(x: ReaL y: Real) p := (x, y), x coord = fun() fst(p), y coord = fun() snd(p)

}

Хотя Ада не имеет концепции типа пакета ,она имеет определение понятия шаблона пакета , который имеет некоторые ,но не все свойства типа.Шаблоны пакетов вводятся ключевым словом generic

generic

package Pointl is

function makepoint (x:ReaL у:Real) return Point; function x coord [P:Point) return Real; function y coord [PPoint) return Real; end Pointl:

Значения point1 и point2 шаблонного пакета Point1 могут быть введены как:

package pointl is new Pointl package point2 is new Pointl

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

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

type p is Point;

p = pointl. makepoint(3,4);

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

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

Конструкция let в предыдущем примере использовалась для реализации сокрытия информации. Мы называем это сокрытие информации первого порядка ,так как это достигается ограничением области действий уровня значений.Это можно противопоставить с сокрытием инфоормации второго порядка ,которое реализуется с помощью кваторов существования , которые ограничивают область действия на уровне типов.

В Ада пакет point2 с приватным типом Point может быть определен как :

package point2

type Point is private;

function makepoint (к:Real, у:Real) return Point; function x coord (P Point) return Real: function y coord (P Point) return Real; private

- hidden local definition of the type Point end poin(2;

Приватный тип Point может быть смоделирован при помощи кваторов существования.

type Point2 = BPoint.

{makepoint: (Real * Real) -> Point x coord: Point -> Reat y coord: Point -» Real

:

Иногда удобно представлять определение типа экзистенционально квантифицированного типа как параметрическую функцию от скрытого параметра-типа. В примере мы можем определить Point2WRT[Point] так:

type Point2WRT[ Point] =

{makepoint: {Real * Real) -> Point x coord: Point -» Real, y coord: Point -» Real

}

Нотация WRT в Point2WRT должна читаться как , подчеркивает тот факт ,что это определение типов соотносится с парамертром-типом. Значие point2 экзистенционального типа Point2 может быть создан операцией pack.

value point2 : Point2 = pack [Point = (Real * Real) in Point2WRT[Point]; pointl

Оперция pack скрывает представление Real*Real типа Point и имеет экзистенционально параметризируемый тип Point2WRT[Point] как часть своего определения и предоставляет как свой скрытые тело предыдуще определеного типа point1 , который реализукет операции для данного представления данных.

Заметьте , что Point2WRT[Point] представляет параметризированный типовое выражение ,которое предоставляется с фактическим параметром таким как Real , устанавливает тип ( в случае типа записи с тремя компонентами).Отношение между ътим типом параметризации и дургим видом параметризации представленным только недавно проиллюстрированы ниже:

1. Функциональная абстракция : fun(x:type) value-expr(x).Параметр х это значение и результат подстановки фактического параметра вместо формального определяет значение. 2.Квантификация :all(a) value-expr(a).Парамеир а это тип и результат подстановки фактического параметра вместо формального определяет значение. 3. Абстракция типов.TypeWRT[T] = type -expr(T).Параметр Т это тип ,результат подстановки формального параметрав вместо фактического тоже тип.

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

Экзистенцональная квантификация может быть использована для моделирвания приватных типов в Ада. Однако , они более общие нежели чем средства абстракции данных в Ада , как покахано в следующем примерах.

5.3 Комбинирования универсальной и экзистенциональной квантификации.

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

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