Приложение 20. Использование формальных спецификаций

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

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

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

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

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

Эти предложения должны появляться в указанном ниже порядке, однако предложения requires и modifies обязательными не являются.

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

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

Рис.1

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

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

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

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

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

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

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

Чтобы специфицировать процедуры, которые вызывают исключительные ситуации, в спецификацию следует добавить предложение signals (рис.2). Это предложение - часть заголовка. Оно следует за предложением returns. Если исключительных ситуаций не имеется, оно может быть опущено.

Шаблон спецификации для процедурных абстракций, обрабатывающих исключительные ситуации

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

Рис.2

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

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

Абстракции данных

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

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

Шаблон спецификации для абстракции типа данных

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

Рис.3

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

В секции операций содержатся спецификации для всех операций.

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

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

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

Абстракции итерации

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

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

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

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

Как и другие абстракции, итераторы должны быть определены через спецификации. Форма спецификации итератора (рис.4) аналогична форме для процедуры.

Шаблон спецификации абстракции итератора

-------------------------------------------------------------------¬
¦ iter_name = iter(входные данные) yields (выходные данные)	   ¦
¦	      signals (сообщения об исключительных ситуациях)	   ¦
¦      requires	 - этот	оператор задает необходимые требования	   ¦
¦      effects	 - этот	оператор описывает выполняемые функции	   ¦
L-------------------------------------------------------------------

Рис.4

Ключевое слово iter используется для обозначения абстракции итератора и содержит входные данные. Итератор может совсем не выдавать объектов на каждой итерации или выдать несколько объектов. Число и тип этих объектов описываются в предложении yields. Итератор может не выдавать никаких результатов, когда он заканчивается нормально, но он может заканчиваться по исключительной ситуации с именем и результатами, указанными в предложении signals.

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

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

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