 |
Специфицирование интерфейсов
|
|
|
|
Большие системы обычно разбиваются на подсистемы, которые разрабатываются независимо друг от друга. Подсистемы могут использовать другие подсистемы, поэтому необходимой частью процесса специфицирования является определение интерфейсов подсистем. Если интерфейсы определены и согласованы, подсистемы можно разрабатывать независимо друг от друга.
Интерфейс подсистемы часто определяется как набор абстрактных типов данных и объектов (рис. 9.4), при этом только через интерфейс доступны описание данных и операции над ними. Поэтому спецификацию интерфейса подсистемы можно рассматривать как объединение спецификаций компонентов, что в итоге и составит описание интерфейса подсистемы.
Рис. 9.4. Объекты интерфейсов подсистем
Точные спецификации интерфейсов подсистем необходимы для разработчиков, которые пишут программный код, обращающийся к сервисам других подсистем. Спецификации интерфейсов содержат информацию о том, какие сервисы доступны в других подсистемах и как получить к ним доступ. Ясный и однозначный интерфейс подсистем уменьшает вероятность ошибок во взаимоотношениях между ними.
Алгебраический подход первоначально был разработан для описания интерфейсов абстрактных типов данных, где типы данных определяются скорее спецификациями операций над данными, чем способом представления самих данных. Это очень похоже на определение классов объектов. Алгебраический подход к формальным спецификациям определяет абстрактный тип данных в терминах операций над данными.
Первый метод спецификации абстрактных типов данных описан в работе [143]. В [78] этот метод был расширен, чтобы предоставить возможность создания завершенной системной спецификации. Одновременно была разработана алгебраическая спецификация абстрактных типов данных [220]. В этой связи отметим, что, вероятно, наилучшим из известных языков алгебраической спецификации является LARCH [145].
|
|
|
Структура спецификации объекта показана на рис. 9.5 и состоит из четырех компонентов.
• Введение, где объявляется класс (sort) объектов. Класс – это общее название для множества объектов. Он обычно реализуется как тип данных. Введение может также включать объявление импорта (imports), где указываются имена спецификаций, определяющие другие классы. Импортирование спецификаций делает эти классы доступными для использования.
• Описательная часть, в которой неформально описываются операции, ассоциированные с классом. Это делает формальную спецификацию более простой для понимания. Формальная спецификация дополняет это описание, обеспечивая однозначный синтаксис и семантику операций.
• Часть сигнатур, в которой определяется синтаксис интерфейса объектного класса или абстрактного типа данных. Здесь описываются имена операций, количество и типы их параметров, а также классы выходных результатов операций.
• Часть аксиом, где определяется семантика операций посредством создания ряда аксиом, которые характеризуют поведение абстрактного типа данных. Эти аксиомы связывают операции создания объектов класса с операциями, проверяющими их значения.
Рис. 9.5. Структура алгебраической спецификации
Процесс разработки формальной спецификации интерфейса подсистемы включает следующие действия.
1. Структурирование спецификации. Представление неформальной спецификации интерфейса в виде множества абстрактных типов данных или объектных классов. Также неформально определяются операции, ассоциированные с каждым классом.
2. Именование спецификаций. Задаются имена для каждой спецификации абстрактного типа, определяются параметры спецификаций (если они необходимы) и имена определяемых классов.
|
|
|
3. Определение операций. На основании списка выполняемых интерфейсом функций для каждой спецификации определяется связанный с ней набор операций. Необходимо предусмотреть операции по созданию экземпляров классов, по изменению значений экземпляров классов и по проверке этих значений. Вероятно, придется добавить новые функции к первоначально определенному списку функций интерфейса.
4. Неформальная спецификация операций. Написание неформальной спецификации для каждой операции, где должно быть указано, как операции воздействуют на определяемый класс.
5. Определение синтаксиса операций. Определение синтаксиса и параметров для каждой операции. Это часть сигнатуры формальной спецификации.
6. Определение аксиом. Определение семантики операций путем описания условий, которые должны выполняться для различных комбинаций операций.
Для пояснения методики алгебраической спецификации, рассмотрим простую структуру данных связанного списка, спецификация которого показана на рис. 9.6.
Предположим, что первый этап разработки спецификации списка, а именно структурирование спецификации, выполнен. Имя спецификации и имя класса может быть одним и тем же, хотя полезно проводить различие между ними, используя какое-либо соглашение. Например, я использую заглавные буквы для имени спецификации (LIST) и прописные буквы с первой заглавной буквой для имени класса (List). Поскольку списки могут содержать элементы разных типов, спецификация имеет общий параметр Elem (Элемент). Тип Elem может представлять целое число, строку, список и т.д.
Рис. 9.6. Спецификация связанного списка
В общем случае для каждого абстрактного типа данных набор необходимых операций должен содержать операцию по созданию нового экземпляра этого типа данных и операцию по конструированию экземпляра данного типа из имеющихся элементов (в нашем примере это операции Create и Cons). В случае применения списков также должны быть операции для получения значения первого элемента списка (в нашем примере операция Head), операция, которая изменяет список путем удаления его первого элемента (Tail), и операция подсчета количества элементов в списке (Length).
|
|
|
При определении синтаксиса этих операций следует установить, какие для них необходимы параметры и каковы должны быть результаты операций. В общем случае входные параметры принадлежат или определяемому классу (в данном случае класс List) или более общему (родовому) классу. Результаты операций также принадлежат тем же классам или некоторому другому, например Integer или Boolean; операция Length возвращает целое число. Декларация импорта, объявляющая использование спецификации целых чисел, должна быть включена в спецификацию. Аксиомы, определяющие семантику абстрактного типа данных, написаны с использованием ранее определенных операций.
Операции над абстрактным типом данных обычно относятся к одному из двух классов.
1. Операции конструирования, которые создают или изменяют объекты класса. Обычно их называют Create (Создать), Update (Изменить), Add (Добавить) или, как в нашем случае, Cons (Конструирование).
2. Операции проверки, которые возвращают атрибуты класса. Обычно им дают имена, соответствующие именам атрибута, или имена, подобные Eval (Значение), Get (Получить) и т.п.
Хорошим эмпирическим правилом для написания алгебраической спецификации является создание аксиом для каждой операции конструирования с применением всех операций проверки. Это означает, что если есть m операций конструирования и n операций проверки то должно быть определено m x n аксиом.
Операции конструирования, связанные с абстрактным типом данных, часто очень сложны и могут определяться через другие операции конструирования и проверки. Если операции конструирования определены посредством других операций, то необходимо определить операции проверки, используя более примитивные конструкции.
В спецификации списка операциями конструирования являются Create, Cons и Tail, которые создают списки. Операциями проверки являются Head и Length, которые используются для получения значений атрибутов списка. Операция Tail не является примитивной конструкцией, поэтому для нее можно не определять аксиомы с использованием операций Head и Length, но в таком случае Tail необходимо определить посредством примитивных конструкций.
|
|
|
При написании алгебраических спецификаций часто используется рекурсия. Результат операции Tail - список, сформированный из входного списка путем удаления верхнего элемента. Это определение подсказывает, как использовать рекурсию для построения данной операции. Операция определяется на пустых списках, затем рекурсивно переходит на непустые списки и завершается, когда результатом снова будет пустой список.
Иногда проще понять рекурсивные преобразования, используя короткий пример. Предположим, что есть список [5, 7], где элемент 5 - начало (вершина) списка, а элемент 7 - конец списка. Операция Cons([5, 7], 9) должна возвратить список [5, 7, 9], а операция Tail, примененная к этому списку, должна возвратить список [7, 9]. Приведем последовательность рекурсивных преобразований, приводящую к этому результату.
Tail ([5, 7, 9]) =
= Tail (Cons ([5, 7], 9)) =
= Cons (Tail ([5, 7]), 9) =
= Cons (Tail (Cons ([5], 7)), 9) =
= Cons (Cons (Tail ([5]), 7), 9) =
= Cons (Cons (Tail (Cons ([], 5)), 7), 9) =
= Cons (Cons ([Create], 7), 9) =
= Cons ([7], 9) =
= [7, 9]
Здесь систематически использовались аксиомы для Tail, что привело к ожидаемому результату. Аксиому для операции Head можно проверить подобным способом.
Теперь рассмотрим, как эту методику можно использовать при разработке спецификации критической системы. Предположим, что имеется система управления воздушным движением, целью которой является контроль за определенным сектором воздушного пространства. В каждом контролируемом секторе может находиться несколько самолетов, имеющих различные идентификаторы. Из соображений безопасности все самолеты должны быть разведены по высоте по крайней мере на 300 метров. В случае попытки каким-либо самолетом нарушить это ограничение, система должна выдать предупреждающий сигнал.
Рис. 9.7. Спецификация класса Sector, представляющего сектор контролируемого воздушного пространства
Чтобы упростить описание, я определил только ограниченное число операций над объектом-сектором. В реальной системе, конечно, будет намного больше операций и более сложными будут условия безопасности полета самолетов. Основные операции следующие.
1. Enter (Ввод). Добавляет самолет (представляемый идентификатором) в воздушное пространство на указанной высоте. На этой высоте или на расстоянии ближе 300 метров от него не должно быть другого самолета.
2. Leave (Выход). Удаляет указанный самолет из контролируемого сектора. Она применяется, если самолет перемещается в соседний сектор.
|
|
|
3. Move (Перемещение). Перемещает самолет с одной высоты на другую. Опять проверяются условия безопасности – расстояние между самолетами должно быть не менее 300 метров.
4. Lookup (Просмотр). Определяет текущую высоту самолета в секторе.
Определение этих операций упростится, если определены также другие операции.
1. Create (Создать). Стандартная операция для любого абстрактного типа данных. Она создает пустой экземпляр данного типа. В нашем случае эта операция задает сектор, в котором отсутствуют самолеты.
2. Put (Поместить). Более простая версия операции Enter. Она добавляет новый самолет в сектор без проверки ограничений.
3. In-space (Проверка пространства). Возвращает значение истины, если указанный самолет находится в контролируемом секторе, в противном случае ее значение ложно.
4. Occupied (Занятый). Возвращает значение истины, если внутри 300-метровой зоны по высоте есть самолет, в противном случае ее значение ложно.
Простые операции определяются для того, чтобы впоследствии использовать их как блоки для компоновки более сложных операций. Алгебраическая спецификация класса Sector (Сектор) показана на рис. 9.7.
По существу, основными операциями конструирования являются Create и Put, которые использованы в спецификациях других операций. Occupied и In-space являются операциями проверки, которые определяют использование операций Create и Put. Как выполняются эти и другие операции, легко понять из спецификации.
|
|
|
