2. Специфицирование інтерфейсів

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

Інтерфейс підсистеми часто визначається як набір абстрактних типів даних і об'єктів (рис. 6.4), при цьому тільки через інтерфейс доступні опис даних і операції над ними. Тому специфікацію інтерфейсу підсистеми можна розглядати як об'єднання специфікацій компонентів, що в підсумку і складе опис інтерфейсу підсистеми.

Рис. 6.4. Об'єкти інтерфейсів підсистем

Точні специфікації інтерфейсів підсистем необхідні для розробників, які пишуть програмний код, що звертається до сервісів інших підсистем. Специфікації інтерфейсів містять інформацію про те, які сервіси доступні в інших підсистемах і як одержати до них доступ. Ясний і однозначний інтерфейс підсистем зменшує ймовірність помилок у взаєминах між ними.

Алгебраїчний підхід спочатку був розроблений для опису інтерфейсів абстрактних типів даних, де типи даних визначаються скоріше специфікаціями операцій над даними, чим способом представлення самих даних. Це дуже схоже на визначення класів об'єктів. Алгебраїчний підхід до формальних специфікацій визначає абстрактний тип даних у термінах операцій над даними.

Структура специфікації об'єкта показана на рис. 6.5 і складається із чотирьох компонентів.

• Введення, де оголошується клас (sort) об'єктів. Клас ‒ ця загальна назва для безлічі об'єктів. Він зазвичай реалізується як тип даних. Введення може також включати оголошення імпорту(imports), де вказуються імена специфікацій, що визначають інші класи. Імпортування специфікацій робить ці класи доступними для використання.

• Описова частина, у якій неформально описуються операції, асоційовані із класом. Це робить формальну специфікацію більш простою для розуміння. Формальна специфікація доповнює цей опис, забезпечуючи однозначний синтаксис і семантику операцій.

• Частини сигнатур, у якій визначається синтаксис інтерфейсу об'єктного класу або абстрактного типу даних. Тут описуються імена операцій, кількість і типи їх параметрів, а також класи вихідних результатів операцій.

• Частини аксіом, де визначається семантика операцій за допомогою створення ряду аксіом, які характеризують поведінку абстрактного типу даних. Ці аксіоми зв'язують операції створення об'єктів класу з операціями, що перевіряють їх значення.

Рис. 6.5. Структура алгебраїчної специфікації

Процеси розробки формальної специфікації інтерфейсу підсистеми включає наступні дії

1. Структурування специфікації.Представлення неформальної специфікації інтерфейсу у вигляді безлічі абстрактних типів даних або об'єктних класів. Також неформально визначаються операції, асоційовані з кожним класом.

2. Іменування специфікацій.Задаються імена для кожної специфікації абстрактного типу, визначаються параметри специфікацій (якщо вони необхідні) і імена обумовлених класів.

3. Визначення операцій.На підставі списку виконуваних інтерфейсом функцій для кожної специфікації визначається пов'язаний з нею набір операцій. Необхідно передбачити операції по створенню екземплярів класів, по зміні значень екземплярів класів і по перевірці цих значень. Імовірно, прийде додати нові функції до спочатку певного списку функцій інтерфейсу.

4. Неформальна специфікація операцій.Написання неформальної специфікації для кожної операції, де повинно бути зазначене, як операції впливають на обумовлений клас.

5. Визначення синтаксису операцій.Визначення синтаксису і параметрів для кожної операції. Це частина сигнатури формальної специфікації.

6. Визначення аксіом.Визначення семантики операцій шляхом опису умов, які повинні виконуватися для різних комбінацій операцій.

Для пояснення методики алгебраїчної специфікації, розглянемо просту структуру даних зв'язаного списку, специфікація якого показана на рис. 6.6.

Припустимо, що перший етап розробки специфікації списку, а саме структурування специфікації, виконаний. Імена специфікації і ім'я класу може бути тим самим, хоча корисно проводити відмінність між ними, використовуючи яку-небудь угоду. Наприклад, використовуються заголовні букви для імені специфікації (LIST) і прописні букви з першою заголовною буквою для імені класу (List). Оскільки списки можуть містити елементи різних типів, специфікація має загальний параметр Elem (Елемент). Тип Elem може представляти ціле число, рядок, список і т.д.

Рис. 6.6. Специфікація зв'язаного списку

У загальному випадку для кожного абстрактного типу даних набір необхідних операцій повинен містити операцію по створенню нового екземпляра цього типу даних і операцію по конструюванню екземпляра даного типу з наявних елементів (у нашому прикладі це операції Create іCons). У випадку застосування списків також повинні бути операції для одержання значення першого елемента списку (у нашому прикладі операціяHead), операція, яка змінює список шляхом видалення його першого елемента(Tail), і операція підрахунку кількості елементів у списку(Length).

При визначенні синтаксису цих операцій слід установити, які для них необхідні параметри і які повинні бути результати операцій. У загальному випадку вхідні параметри належать або обумовленому класу (у цьому випадку клас List) або більш загальному (родовому) класу. Результати операцій також належать тим же класам або деякому іншому, наприкладInteger абоBoolean; операціяLength повертає ціле число. Декларація імпорту, що повідомляє використання специфікації цілих чисел, повинна бути включена в специфікацію. Аксіоми, що визначають семантику абстрактного типу даних, написані з використанням раніше визначених операцій.

Операції над абстрактним типом даних зазвичай відносяться до одного із двох класів.

1. Операції конструювання,які створюють або змінюють об'єкти класу. Зазвичай їх називаютьCreate (Створити),Update (Змінити),Add (Додати) або, як у нашому випадку,Cons (Конструювання).

2. Операції перевірки, які повертають атрибути класу. Зазвичай їм дають імена, відповідні до імен атрибута, або імена, подібніEval (Значення),Get (Одержати) і т.п.

Гарним емпіричним правилом для написання алгебраїчної специфікації є створення аксіом для кожної операції конструювання із застосуванням усіх операцій перевірки. Це означає, що якщо є mоперацій конструювання іпоперацій перевірки, то повинно бути визначеноm хп аксіом.

Операції конструювання, пов'язані з абстрактним типом даних, часто дуже складні і можуть визначатися через інші операції конструювання і перевірки. Якщо операції конструювання визначені за допомогою інших операцій, то необхідно визначити операції перевірки, використовуючи більш примітивні конструкції.

У специфікації списку операціями конструювання є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 метрів. У випадку спроби яким-небудь літаком порушити це обмеження, система повинна видати попереджуючий сигнал.

Рис. 6.7.Специфікація класу Sector, що представляє сектор контрольованого повітряного простору

Щоб спростити опис, визначається тільки обмежене число операцій над об'єктом-сектором. У реальній системі, зазвичай, буде набагато більше операцій і більш складними будуть умови безпеки польоту літаків. Основні операції наступні.

1. Enter (Введення). Додає літак (який представляється ідентифікатором) у повітряний простір на зазначеній висоті. На цій висоті або на відстані ближче 300 метрів від нього не повинно бути іншого літака.

2. Leave (Вихід). Видаляє зазначений літак з контрольованого сектору. Вона застосовується, якщо літак переміщається в сусідній сектор.

3. Move (Переміщення). Переміщає літак з однієї висоти на іншу. Знову перевіряються умови безпеки ‒ відстань між літаками повинна бути не менше 300 метрів.

4. Lookup(Перегляд). Визначає поточну висоту літака в секторі.

Визначення цих операцій спроститься, якщо визначені також інші операції.

1. Create (Створити). Стандартна операція для будь-якого абстрактного типу даних. Вона створює порожній екземпляр даного типу. У нашому випадку ця операція задає сектор, у якому відсутні літаки.

2. Put (Помістити). Більш проста версія операціїEnter. Вона додає новий літак у сектор без перевірки обмежень.

3. In-space (Перевірка простору). Повертає значення істини, якщо зазначений літак знаходиться в контрольованому секторі, а якщо ні, то її значення неправильне.

4. Occupied(Зайнятий). Повертає значення істини, якщо усередині 300-метрової зони по висоті є літак, а якщо ні, то її значення неправильне.

Прості операції визначаються для того, щоб згодом використовувати їх як блоки для компонування більш складних операцій. Алгебраїчна специфікація класу Sector (Сектор) показана на рис. 6.7.

По суті, основними операціями конструювання є Create іPut, які використані в специфікаціях інших операцій.Occupied іIn-space є операціями перевірки, які визначають використання операційCreate іPut. Як виконуються ці і інші операції, легко зрозуміти зі специфікації.