1. Использование абстракций и спецификаций в разработке ПО

1.1. Абстракции программы

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

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

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

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

---------------------------------------------------------------------¬
¦ ¦
¦-------------¬ -----------------¬ -------------¬¦
¦¦ Ввод ¦ исходная ¦ Преобразование ¦преобразов. ¦ Вывод ¦¦
¦¦ ¦=========>¦ ¦===========>¦ ¦¦
¦¦ информации ¦информация¦ информации ¦информация ¦ информации ¦¦
¦L------------- L----------------- L-------------¦
¦ ¦ ¦
¦ Выходная ¦ ¦
¦ <==============- ¦
¦ информация ¦
L---------------------------------------------------------------------

Рис.1.1.Абстракция программы как набора процедур, обрабатывающих данные.

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

---------------------------------------------------------------------¬
¦ Управляющая ¦
¦ ====================¬ ¦
¦ информация ¦ ¦
¦ ¦ ¦
¦ v ¦
¦ ------------¬ ¦
¦ Входная ¦ ¦ Выходная ¦
¦ ====================>¦ Процедура ¦====================> ¦
¦ информация ¦ ¦ информация ¦
¦ L------------ ¦
¦ ¦
L---------------------------------------------------------------------

Рис.1.2.Абстракция процедуры

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

---------------------------------------------------------------------¬
¦ Ввод ¦
¦ г=============== ¦
¦ ¦ информации ¦
¦ v ¦
¦-------------¬ -------------¬¦
¦¦ Исходная ¦ Преобразование ¦ Выходная ¦¦
¦¦ ¦==================¬ г===>¦ ¦¦
¦¦ информация ¦ информации ¦ ¦ ¦ информация ¦¦
¦L------------- ¦ ¦ L-------------¦
¦ г============- ¦ ¦
¦ ¦ L=====¬ ¦
¦ ¦ ------------------¬ ¦ ¦
¦ ¦ ¦ Преобразованная ¦ Вывод ¦ ¦
¦ L==>¦ ¦=============- ¦
¦ ¦ информация ¦ информации ¦
¦ L------------------ ¦
¦ ¦
L---------------------------------------------------------------------

Рис.1.3.Абстракция программы как набора данных, обрабатываемых процедурами.

Анализ рис.1.3 позволяет также получить абстракцию данных.

---------------------------------------------------------------------¬
¦ Процедуры ¦
¦ =================¬ ¦
¦ управления ¦ ¦
¦ v ¦
¦ -----------¬ ¦
¦ Процедуры ¦ ¦ Процедуры ¦
¦ ================>¦ Данные ¦===============> ¦
¦ ввода ¦ ¦ вывода ¦
¦ L----------- ¦
¦  ¦
¦ Процедуры ¦ ¦
¦ =================- ¦
¦ преобразования ¦
L---------------------------------------------------------------------

Рис.1.4.Абстракция данных.

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

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

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

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

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

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

При анализе спецификации для уяснения смысла обращения к процедуре следует придерживаться двух правил.

1. После выполнения процедуры можно считать, что конечное условие выполнено.

2. Можно ограничиться только теми свойствами, которые подразумевает конечное условие.

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

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

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

1.2. Процедурная абстракция

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

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

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

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

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

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

Спецификация процедуры состоит из заголовка и описания функции, выполняемой процедурой. Заголовок содержит имя процедуры, номер, порядок и типы входных и выходных параметров. Кроме этого, выходные параметры могут, а входные должны быть поименованы.

Семантическая часть спецификации состоит из трех предложений requires (требует), modifies (модифицирует) и effects (делает). Эти предложения должны появляться в указанном ниже порядке, однако предложения requires и modifies обязательными не являются.

 -------------------------------------------------------------------¬
¦ proc(входные данные) returns (выходные данные) ¦
¦ requires - этот оператор задает необходимые требования ¦
¦ modifies - этот оператор идентифицирует все модифицируемые ¦
¦ входные данные ¦
¦ effects - этот оператор описывает выполняемые функции ¦
L-------------------------------------------------------------------

Рис.1.5.Шаблон спецификации для процедурных абстракций.

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

Оператор modifies задает список имен входных параметров, модифицируемых процедурой. Если входные параметры не указаны, то это предложение может быть опущено.

Предложение effects описывает работу процедуры со значениями, не охваченными предложением requires. Оно определяет выходные значения и модификации, производимые над входными параметрами, перечисленными в в списке modifies. Предложение effects составляется исходя из предположения, что требования предложения requires удовлетворены. Однако в том случае, когда требования в предложении requires не удовлетворены, о поведении процедуры ничего не сообщается.

На рис.1.6 приведено несколько процедурных спецификаций. Процедуры sort и search не изменяют входные данные, а процедура clear - изменяет, что отмечено в предложении modifies ее спецификации. Процедуры sort и clear являются общими процедурами, поскольку их спецификации не содержат предложений requires. Процедура search является частичной; она выполняет свои функции только в том случае, если входной массив отсортирован. Однако в предложении effects ничего не говорится о результатах работы процедуры для неотсортированного входного массива.

Приведенная на рис.1.6 спецификация процедуры sort предназначена для работы с массивом целых чисел. Эта процедура была бы более полезной, если бы могла работать с массивами любых типов данных - действительных чисел, символьных, строковых, вплоть до вводимых пользователем. Для обеспечения подобного обобщения используется абстракция через параметризацию, при которой типы данных являются параметрами.

 -------------------------------------------------------------------¬
¦ ort = proc(a:array of int) returns (b:array of int) ¦
¦ effects - возвращает новый массив той же размерности, ¦
¦ что и a, содержащий элементы из массива a, упоря¦
¦ доченные по возрастанию ¦
L------------------------------------------------------------------ -------------------------------------------------------------------¬
¦ clear = proc(a:array of int) ¦
¦ modifies - a ¦
¦ effects - удаляет из массива a все повторяющиеся элементы ¦
L------------------------------------------------------------------ -------------------------------------------------------------------¬
¦ search= proc(a:array of int;x:int) returns (i:int) ¦
¦ requires - массив a упорядочен по возрастанию ¦
¦ effects - если элемент x принадлежит массиву a, то возвра-¦
¦ щается значение i, такое, что a[i]=x; в против- ¦
¦ ном случае - значение i на единицу большее верх-¦
¦ ней границы массива a ¦
L-------------------------------------------------------------------

Рис.1.6.Спецификации процедурных абстракций.

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

Некоторые спецификации для параметризованных процедур показаны на рис.1.7. Эти спецификации отличаются от спецификаций непараметризован-

 -------------------------------------------------------------------¬
¦ sort = proc[t:type](a:array [t]) returns (array [t]) ¦
¦ requires - t имеет операцию ¦
¦ lt:proctype(t,t) returns(bool), ¦
¦ которая упорядочивает t ¦
¦ modifies - a ¦
¦ effects - возвращает новый массив той же размерности, ¦
¦ что и a, содержащий элементы из массива a, упоря¦
¦ доченные по возрастанию ¦
L------------------------------------------------------------------ -------------------------------------------------------------------¬
¦ search= proc[t:type](a:array [t];x:t) returns (int) ¦
¦ requires - t имеет операции ¦
¦ equal,lt:proctype(t,t) returns (bool), ¦
¦ такие, что t упорядочивается через equal, а ¦
¦ массив a упорядочен по возрастанию через lt ¦
¦ effects - если элемент x принадлежит массиву a, то возвра-¦
¦ щается значение i, такое, что a[i]=x; в против- ¦
¦ ном случае - значение i на единицу большее верх-¦
¦ ней границы массива a ¦
L-------------------------------------------------------------------

Рис.1.7.Спецификации параметризованных процедур.

ных процедур только заголовком, который содержит дополнительную часть,содержащую параметры. Предложение requires помимо прочих ограничений содержит ограничения, накладываемые на параметры. Если ограничения отсутствуют, то предложение requires может быть опущено. Например, абстракция sort требует, чтобы параметр t имел операцию lt, упорядочивающую t. Аналогично процедура search требует, чтобы ее параметр поддерживал как операцию lt, так и операцию equal. (lt - меньше, equal равно).

Параметризованная абстракция в действительности представляет собой класс взаимосвязанных абстракций, определенных в одной спецификации. Спецификация процедуры естественным образом получается из спецификации класса путем замены имени параметра его значением и удалением  из предложения requires ограничений на тип параметра(ов).

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

1.3. Абстракция типа данных

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

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

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

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

Если обеспечено достаточное количество операций, отсутствие доступа к представлению не создаст никаких трудностей для пользователя.

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

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

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

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

      ----------------------------------------------------------¬
¦ Описание ¦
¦ Здесь приводится описание абстракции данных ¦
¦ Операции ¦
¦ Здесь задаются спецификации для всех операций ¦
¦ end dname ¦
L----------------------------------------------------------

Рис.1.8.Общий вид спецификации абстракции данных.

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

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

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

 -------------------------------------------------------------------¬
¦ntset = data type is create, insert, delete, member, size, choose ¦
¦ ¦
¦Описание ¦
¦ ¦
¦ Наборы целых чисел intset - это неограниченные математические ¦
¦ множества целых чисел. Наборы целых чисел изменяемые: операции ¦
¦ insert и delete добавляют и удаляют целые числа из набора. ¦
¦ ¦
¦Операции ¦
¦ ¦
¦ create = proc () returns (intset) ¦
¦ effects возвращает новый, пустой набор intset ¦
¦ ¦
¦ insert = proc (s: intset, x:int) ¦
¦ modifies s ¦
¦ effects добавляет x к элементам s; после добавления - ¦
¦ возврат ¦
¦ ¦
¦ delete = proc (s: intset, x:int) ¦
¦ modifies s ¦
¦ effects удаляет x из s ¦
¦ ¦
¦ member = proc (s:intset, x:int) returns (bool) ¦
¦ effects возвращает значение true, если x принадлежит s ¦
¦ ¦
¦ size = proc (s: intset) returns (int) ¦
¦ effects возвращает число элементов в s ¦
¦ ¦
¦ choose = proc (s: intset) returns (int) ¦
¦ requires набор s не пуст ¦
¦ effects возвращает произвольный элемент s ¦
¦ ¦
¦end intset ¦
L-------------------------------------------------------------------

Рис.1.9.Спецификация типа данных intset.

На рис.1.10 представлена спецификация типа данных poly. Полиномы poly - это неизменяемые полиномы с целыми коэффициентами. Предоставляются операции для создания одночленного полинома, для сложения, вычитания и умножения полиномов, а также для проверки двух полиномов на равенство.

 -------------------------------------------------------------------¬
¦poly = data type is create,degree,coef,add,mul,sub,minus,equal ¦
¦ ¦
¦Описание ¦
¦ ¦
¦ Полиномы poly - это неизменяемые полиномы с целыми коэффициентами¦
¦ ¦
¦Операции ¦
¦ ¦
¦ create = proc (c,n:int) returns (poly) ¦
¦ requires n>=0 n ¦
¦ effects возвращает полином cx. Например, ¦
¦ poly.create(0,0) = 0 ¦
¦ poly.create(3,0) = 3 3 ¦
¦ poly.create(6,3) = 6x ¦
¦ ¦
¦ degree = proc (p: poly) returns(int) ¦
¦ effects возвращает степень p, т.е. наибольшую степень при ¦
¦ ненулевом коэффициенте. Степень нулевого полинома ¦
¦ равна 0. Например, 2 ¦
¦ poly.degree(17) = 0 poly.degree(x +1) = 2 ¦
¦ ¦
¦ coef = proc (p: poly, n:int) returns (int) ¦
¦ requires n>=0 ¦
¦ effects возвращает коэффициент члена p со степенью n. Воз-¦
¦ вращает 0, если n больше степени p. Например, ¦
¦ 3 ¦
¦ poly.coef(x +2x+1,4) = 0 ¦
¦ 3 ¦
¦ poly.coef(x +2x+1,1) = 2 ¦
¦ ¦
¦ add = proc (p,q: poly) returns (poly) ¦
¦ effects возвращает полином, являющийся суммой полиномов p ¦
¦ и q ¦
¦ ¦
¦ mul = proc (p,q: poly) returns (poly) ¦
¦ effects возвращает полином, являющийся произведением поли-¦
¦ номов p и q ¦
¦ ¦
¦ sub = proc (p,q: poly) returns (poly) ¦
¦ effects возвращает полином, являющийся разностью полиномов¦
¦ p и q ¦
¦ ¦
¦ minus = proc (p: poly) returns (poly) ¦
¦ effects возвращает полином, являющийся разностью полиномов¦
¦ z и p, где z - нулевой полином ¦
¦ ¦
¦ equal = proc (p,q: poly) returns (bool) ¦
¦ effects возвращает значение true, если p и q имеют одинако¦
¦ вые коэффициенты при соответствующих членах, и зна¦
¦ чение false - в противном случае ¦
¦ ¦
¦end poly ¦
L-------------------------------------------------------------------


Рис.1.10.Спецификация абстракции данных для полиномов..

Типы - выгодные параметры для данных, как и для процедур. Например, рассмотрим абстракцию общего набора set, в котором элементы набора могут быть произвольного типа. Конечно, не все типы могут быть имеющими смысл параметрами общего набора. Так как общие наборы set не хранят дублирующих друг друга элементов, должен быть некий способ определить, дублируют элементы друг друга или нет. Следовательно, спецификация set, представленная на рис.1.11, требует, чтобы элементы типа имели операцию equal. Эти требования помещены сразу после заголовка.

 -------------------------------------------------------------------¬
¦ set = data type [t:type] is create, insert, delete, member, size,¦
¦ choose ¦
¦ ¦
¦Requires t имеет операцию ¦
¦ equal:proctype(t,t) returns(bool), ¦
¦ то есть условие проверки равенства t ¦
¦ ¦
¦Описание ¦
¦ ¦
¦ Общие наборы set - это неограниченные математические наборы ¦
¦ Эти наборы изменяемые: операции insert и delete добавляют и унич-¦
¦ тожают элементы набора ¦
¦ ¦
¦Операции ¦
¦ ¦
¦ create = proc () returns (set [t]) ¦
¦ effects возвращает новый, пустой набор set ¦
¦ ¦
¦ insert = proc (s: set[t], x:t) ¦
¦ modifies s ¦
¦ effects добавляет x к элементам s; после добавления - ¦
¦ возврат ¦
¦ ¦
¦ delete = proc (s: set[t], x:t) ¦
¦ modifies s ¦
¦ effects удаляет x из s ¦
¦ ¦
¦ member = proc (s: set[t], x:t) returns (bool) ¦
¦ effects возвращает значение true, если x принадлежит s ¦
¦ ¦
¦ size = proc (s: set[t]) returns (int) ¦
¦ effects возвращает число элементов в s ¦
¦ ¦
¦ choose = proc (s: set[t]) returns (t) ¦
¦ requires набор s не пуст ¦
¦ effects возвращает произвольный элемент s ¦
¦ ¦
¦end set ¦
L-------------------------------------------------------------------

Рис.1.11.Спецификация параметризованной абстракции данных.

В качестве параметра для набора set может быть использован тип poly. Например, pset = set[poly].

Poly является законным параметром для абстракции данных set, так как имеет операцию equal.

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

 -------------------------------------------------------------------¬
¦list = data type [:type] is create,cons,first,rest,empty,equal ¦
¦ ¦
¦Описание ¦
¦ ¦
¦ Списки - это неизменяемые неограниченные последовательности ¦
¦ элементов типа t ¦
¦ ¦
¦Операции ¦
¦ ¦
¦ create = proc () returns (list [t]) ¦
¦ effects возвращает новый, пустой список ¦
¦ ¦
¦ cons = proc (x: list[t], i:t) returns(list[t]) ¦
¦ effects возвращает список, у которого первый элемент i, а ¦
¦ остальные элементы - элементы x ¦
¦ ¦
¦ first = proc (x: list[t]) returns(t) ¦
¦ requires x - не пуст ¦
¦ effects возвращает первый элемент x ¦
¦ ¦
¦ rest = proc (x: list[t]) returns (list[t]) ¦
¦ requires x - не пуст ¦
¦ effects возвращает список, содержащий все элементы x, кро-¦
¦ ме первого ¦
¦ ¦
¦ empty = proc (x: list[t]) returns (bool) ¦
¦ effects возвращает значение true, если x - пуст, и значе- ¦
¦ ние false - в противном случае ¦
¦ ¦
¦ equal = proc (x,y: list[t]) returns (bool) ¦
¦ requires t имеет операцию ¦
¦ equl:proctype(t,t) returns(bool), ¦
¦ то есть условие равенства t ¦
¦ effects возвращает значение true, если x и y содержат оди-¦
¦ наковые (в соответствии с t.equal) и одинаково рас¦
¦ положенные элементы ¦
¦ ¦
¦end list ¦
L-------------------------------------------------------------------


Рис.1.12.Спецификация параметризованной абстракции данных для списков.

Следует заметить, что списки как целое не налагают никаких требований на тип параметра. Таким образом, list[intset] - законный тип.

Однако операция equal должна проверять элементы на равенство, поэтому она в предложении requires налагает на t требования. Следовательно, list[intset] имеет все операции списков, кроме операции equal, так как intset не имеет операции equal.

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

 -------------------------------------------------------------------¬
¦list = data type [t:type] is create,addel,remel,is_in,empty,least ¦
¦ ¦
¦Requires - t имеет операции ¦
¦ equal,lt:proctype(t,t) returns (bool), ¦
¦ которые определяют упорядочение t ¦
¦ ¦
¦Описание ¦
¦ ¦
¦Упорядоченные списки olist - изменяемые списки элементов. Операции¦
¦addel и remel модифицируют списки. Каждый элемент упорядоченного ¦
¦списка отличается от остальных (как определяется t.equal). Опера- ¦
¦ция least возвращает наименьший элемент olist (как определяется ¦
¦t.lt) ¦
¦ ¦
¦Операции ¦
¦ ¦
¦ create = proc () returns (olist [t]) ¦
¦ effects возвращает новый, пустой список ¦
¦ ¦
¦ addel = proc (s: olist[t], x:t) ¦
¦ requires x не содержится в s; т.е. обращение к is_in(s,x) ¦
¦ возвращает false ¦
¦ modifies s ¦
¦ effects вставляет x в s ¦
¦ ¦
¦ remel = proc (s: olist[t], x:t) ¦
¦ requires x содержится в s; т.е. обращение к is_in(s,x) ¦
¦ возвращает true ¦
¦ modifies s ¦
¦ effects удаляет x из s ¦
¦ ¦
¦ is_in = proc (s: olist[t], x:t) returns (bool) ¦
¦ effects возвращает значение true, если s содержит элемент ¦
¦ равный x (используется t.equal), в противном слу- ¦
¦ чае возвращает значение false ¦
¦ ¦
¦ empty = proc (s: olist[t]) returns (bool) ¦
¦ effects возвращает значение true, если s не содержит эле- ¦
¦ ментов, и значение false - в противном случае ¦
¦ ¦
¦ least = proc (s: olist[t]) returns(t) ¦
¦ requires список не пуст, то есть обращение к операции ¦
¦ empty(s) возвращает значение false ¦
¦ effects возвращает элемент e из s, такой, что в s не суще-¦
¦ ствует элемента, меньшего e(как определяется t.lt)¦
¦ ¦
¦end olist ¦
L-------------------------------------------------------------------

Рис.1.13.Спецификация параметризованной абстракции данных для упорядоченных списков.

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

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

Операции абстракции данных распадаются на четыре класса.

1) Примитивные конструкторы. Эти операции создают объекты соответствующего им типа, не используя никаких объектов в качестве аргументов. (Операция create для наборов intset).

2) Конструкторы. Эти операции используют в качестве аргументов объекты соответствующего им типа и создают другие объекты такого же типа. (Операции add и mul - конструкторы для полиномов, операции cons и rest - конструкторы для списков).

3) Модификаторы. Эти операции модифицируют объекты соответствующего им типа. (Операции insert и delete - модификаторы для наборов intset). Очевидно, что только изменяемые типы могут иметь модификаторы.

4) Наблюдатели. Эти операции используют в качестве аргументов объекты соответствующего им типа и возвращают результат другого типа. Они используются для получения информации об объектах. (Операции size, member и choose для наборов intset, операции coef, degree и equal для полиномов).

Обычно примитивные конструкторы создают не все, а только некоторые объекты. Например, операция poly.create создает только одночленные полиномы, а операция intset.create создает только пустой набор.

Другие объекты создаются конструкторами или модификаторами. Например, операция poly.add может быть использована для получения полиномов, у которых количество членов больше одного, а операция intset.insert для получения наборов с многими элементами.

Модификаторы играют ту же роль для изменяемых типов, что и конструкторы для неизменяемых. Изменяемый тип может иметь как конструкторы, так и модификаторы; например, наборы intset могут иметь операцию copy, которая создает новый набор, содержащий те же элементы, что и ее аргумент. Иногда наблюдатели комбинируются с конструкторами или модификаторами; например, операция remel для упорядоченных списков olist с помощью операций least и remel может модифицировать список и возвратить удаленный элемент.

Тип данных является полным, если он обеспечивает достаточно операций для того, чтобы все требующиеся пользователю работы с объектами могли быть проделаны с приемлемой эффективностью. Строгое определение полноты дать невозможно, хотя существуют пределы относительно того, насколько мало операций может иметь тип, оставаясь при этом приемлемым. Например, если для наборов intset будут существовать только операции create, insert и delete, то программы не смогут получить никакой информации относительно элементов набора (так как не имеется наблюдателей). Если к этим трем операциям добавить только одну - size, то уже возможно получение информации об элементах набора (например, можно проверять на принадлежность, удаляя целые числа и анализируя, изменился ли размер). Но тип в этом случае получится неэффективным и неприемлемым.

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

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

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

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

Для доказательства используется метод индукции. Чтобы установить инвариант абстракции необходимо показать, что он сохраняется для всех объектов, произведенных типом. Как правило, используется следующий метод.

1) Показать, что свойство сохраняется для всех объектов, возвращаемых примитивными конструкторами.

2) Показать, что свойство сохраняется для объектов, возвращаемых конструкторами, предполагая, что свойство сохраняется для объектов, передаваемых конструкторам в качестве аргументов.

3) Показать, что при выходе из модификатора свойство сохраняется для модифицированных объектов, предполагая, свойство сохраняется при вызове модификатора.

Например, упорядоченные списки (рис.1.13) не содержат дублирующих элементов. Этот инвариант полезен для определения корректности реализации наборов intset с использованием упорядоченных списков. То, что это свойство является инвариантом, устанавливается следующим образом:

1) оно сохраняется для единственного примитивного конструктора create, так как операция create возвращает новый пустой список;

2) оно сохраняется для операции addel(s,x). При возврате из этой операции в s содержатся те же элементы, которые там были до вызова, плюс элемент x. По предположению, до вызова в s не было дублирующих друг друга элементов. Кроме того, операция addel требует (в предложении requires), чтобы x не содержался в s. Следовательно, набор s с добавленным элементом x не содержит дублирующих друг друга элементов;

3) оно сохраняется для операции remel(s,x), так как оно сохраняется для s (по предположению), а операция remel только удаляет элементы из s.

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