Курсова - Додаток 20. Використання формальних специфікацій
Химия

Курсова — Додаток 20. Використання формальних специфікацій


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

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

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

Специфікація процедури (рис.1) складається із заголовка та опису функції, що виконується процедурою. Заголовок містить ім’я процедури, номер, порядок та типи вхідних та вихідних параметрів.

Семантична частина специфікації складається з трьох пропозицій — requires (вимагає), modifies (модифікує) та effects (виконує).

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

Специфікації шаблон для процедурних абстракцій

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

Рис.1

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

Оператор modifies задає список імен вхідних параметрів, що модифікуються процедурою. Якщо вхідні параметри не вказані, ця пропозиція може бути опущена.

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

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

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

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

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

Щоб специфікувати процедури, що викликають виняткові ситуації, до специфікації слід додати пропозицію signals (рис.2). Ця пропозиція – частина заголовка. Воно слідує за пропозицією returns. Якщо виняткових ситуацій немає, воно може бути опущене.

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

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

Рис.2

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

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

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

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

Також як для процедур значення типу не повинно задаватися ніякою його реалізацією. Натомість повинна бути визначальна його специфікація. Оскільки об’єкти типу використовуються лише викликом операцій, переважна більшість специфікації присвячена опису те, що ці операції роблять. Загальний вид специфікації даних складається з заголовка, що визначає ім’я типу та імена його операцій, та двох головних секцій — секції опису та секції операцій (рис.3).

Специфікації шаблон для абстракції типу даних

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

Рис.3

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

У секції операцій містяться специфікації всім операцій.

Якщо операція – процедура, то її специфікація буде процедурною специфікацією. У цих специфікаціях можуть бути використані концепції, введені в секції опису.

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

Акцент на взаємозв’язках між операціями робить абстракцію даних суттєво відмінною від набору процедур.

Абстракції ітерації

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

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

Слід зазначити поділ обов’язків у такій формі взаємодії. Ітератор відповідальний за отримання елемента, а модуль, що містить цикл, визначає ту дію, яка буде над ним виконуватись.

Ітератори є деякою узагальненою формою методів ітерації, що є у більшості мов програмування.

Як і інші абстракції, ітератори мають визначити через специфікації. Форма специфікації ітератора (рис.4) аналогічна формі процедури.

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

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

Рис.4

Ключове слово iter використовується для позначення абстракції ітератора та містить вхідні дані. Ітератор може зовсім не видавати об’єктів кожної ітерації чи видати кілька об’єктів. Число і тип цих об’єктів описуються у пропозиції yields. Ітератор може не видавати жодних результатів, коли він закінчується нормально, але він може закінчуватися за винятковою ситуацією з ім’ям та результатами, вказаними у пропозиції signals.

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

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

Ітератори корисні власними силами, проте їх основним застосуванням є операції з типами даних.

© Реферат плюс



Добавить комментарий

Ваш адрес email не будет опубликован. Обязательные поля помечены *