Розробка сучасного ПО супроводжується рядом дій, спрямованих на поліпшення його якості. Одним з таких методів є проектування за контрактом.
Як і будь-який інший, цей метод не є панацеєю від помилок дизайну і кодування, але дозволяє в значній мірі формалізувати обидва ці процеси. Формалізація охоплює і взаємовідносини самих розробників, оскільки даний метод належить до групи самодокументіруемих: специфікації описуються безпосередньо в програмі, а не в супроводжуючих документах.
«Проектування за контрактом» - це переклад англійського терміна «Design by Contract *. Ще один термін, який нам буде потрібно, - «assertion» - твердження.
Історія розглянутого механізму почалася півстоліття тому. У 1950 році на конференції в Кембриджі Алан Тьюринг запропонував включати в програму вимоги, які повинні перевірятися під час її виконання і з яких можна вивести коректність всієї програми. Ідея таких вимог потім розглядалася Флойдом, Хоаром, Дейкстрой і іншими (хтось може згадати знамениті трійки Хоара, описані не в одній книзі по розробці коректних програм).
Для завдання цих вимог були розроблені формальні мови опису специфікацій, такі як Z і VDM, а також їх об'єктно-орієнтовані версії. Однак, що стосується мов програмування, вони практично не забезпечували підтримку опису вимог на рівні мови. Найбільш раннім мовою програмування з подібною підтримкою став Algol W. СШ підтримував опис, що є попередником того, що було розроблено для Ейфеля, але в CLU ці описи були невиконуюча. Саме ж поняття «проектування за контрактом» було вперше введено Мейером в 1987 році і підтримано в Ейфелі. З тих пір воно привертає все більшу увагу з боку розробників інших мов програмування.
Навіть ранні специфікації по Java включали вбудовану підтримку основних механізмів реалізації «проектування за контрактом», але в зв'язку з жорсткими тимчасовими рамками, що обмежують випуск першої версії, вони були згодом відкинуті (як, втім, і ряд інших ГО-механізмів).
3. Чи захищає «захисне програмування»
«Захисне програмування» відомо досить давно: програму треба писати так, щоб вона «розумно» вела себе як на очікуваних, так і на не очікується вхідних даних, тобто щоб не «падала» ні за яких вхідних даних. Насправді, якщо мова йде не про закінчену продукті, а про бібліотеку класів, які можуть використовуватися не в одному проекті, а в різних, даний підхід не тільки не сприяє розробці, але, навпаки, істотно заважає їй.
Розглянемо простий приклад. Нехай потрібно написати функцію обчислення квадратного кореня: sqrt (х: REAL): REAL
-- Повертає квадратний корінь з 'х'
Виникає питання, обробляє вадами слуху негативні аргументи? За правилом «захисту від дурня», треба передбачити таку обробку. На жаль, не ясно, яку саме. Можна для негативних аргументів повертати їх же, або обчислювати для них корінь з протилежного величини аргументу, або видавати повідомлення про помилку (з варіантами: на консоль, в діалогове вікно), або порушувати виняткову ситуацію, або. Тепер уявімо, що треба обчислити вираз arcsin (sqrt (In (х)) / у)
Уявіть, що різні функції були написані різними людьми з використанням «захисного програмування». Відповісти на питання, яке число всіх можливих варіантів поведінки функції при неприпустимих аргументах, надається читачеві.
4. Передумови та постумови
-- Повертає квадратний корінь з 'х' - 'х' має бути невід'ємним
-- Повертає квадратний корінь з 'х' require non_negative_x: х gt; = 0
Тут «require» позначає секцію передумов, наступна за нею рядок - одне з передумов з тегом «non_negative_x» і обчислюваних виразом «х gt; = 0 ». Якщо задано кілька передумов, то для нормального виконання програми всі вони повинні бути щирі. В іншому випадку буде порушена виняткова ситуація.
Тепер перевірка невід'ємності аргументу виконується автоматично при кожному виклику функції sqrt, і про порушення цієї умови буде негайно повідомлено. Наша функція досить проста, і її передумова очевидно. У більш складних випадках правомірне питання: чи завжди можна знайти підходяще передумова? На жаль, відповідь негативна. наприклад:
• завдання передумови функції рівносильно обчисленню самої функції, для якого воно задається (скажімо, знайти значення, факторіал якого дорівнює заданому);
• завдання досить складна для повністю формальної специфікації;
• формальне передумова вимагає введення великої кількості допоміжних функцій, які не мають ніякого сенсу поза рамками даного передумови, і т. П.
-- Повертає квадратний корінь з 'х' require non_negative_x: - 'х' має бути - невід'ємним
-- Повертає квадратний корінь з 'х' - Результат неотрицателен require non_negative_x: х gt; = 0 але, слідуючи формальному стилю, можна переписати так: sqrt (х: REAL): REAL
-- Повертає квадратний корінь з 'х' require non_negative_x: х gt; = 0 ensure non_negative_result: Result gt; = 0
Тепер функція sqrt не тільки накладає обмеження на аргумент, але і гарантує виконання обмежень на результат. Іншими словами, реалізація цієї функції гарантує, що результат буде невід'ємним при неотрицательную аргументі. Однак до функцій з такою властивістю відноситься не тільки функція квадратного кореня. Наприклад, функція, яка завжди повертає 5, також підійде. Це означає, що постусловіем, а саме так називається умова, що знаходиться в секції ensure і обчислює після виконання тіла функції, недостатньо строго. Необхідно додати, що квадрат результату має дорівнювати аргументу. Опцію представлений нижче: sqrt Сх: REAL): REAL
-- Повертає квадратний корінь з 'х' require non_negative_x: х gt; = 0 ensure non_negative_resuIt: Result gt; = 0 definition: Result л 2 - x
Фактично, ми задали в передумовою область визначення функції, а в постусловіем - область її значень і зв'язок між аргументом і результатом. У загальному ж випадку передумова визначає, коли метод може бути нормально виконаний, а постусловіем -що гарантується після його виконання.
Звернемося тепер до реалізації: sqrt (х: REAL): REAL is
-- Повертає квадратний корінь з 'х' require non_negative_x: х gt; = 0 do if х gt; = 0 then
-- обчислення квадратного кореня else
-- обробка помилки end
Щось тут не так: адже ми ж якраз і намагалися уникнути будь-якої обробки помилок. Принцип «ненадлишкових» говорить: не можна перевіряти в тілі рутини умова, заданий в її передумовою. Воно і так істинно. Що ж станеться, якщо передумова буде порушено? На це питання ми відповімо в наступному розділі.
Спочатку повернемося до поняття «проектування але контрактом». Слово «контракт» перш за все явно визначає, що мова йде про формалізацію взаємовідносин між якимись сторонами. В даному випадку одна сторона називається «постачальник» (supplier), а інша - «клієнт» (client). Постачальник бере на себе зобов'язання забезпечити якусь функціональність для клієнта. Але тільки тоді, коли виконані всі передумови. Зі свого боку він гарантує, що після виконання будуть виконані всі постумови. Тим самим проводиться чіткий поділ прав і обов'язків.
Завдяки цьому спрощується сама програма, так як постумови однієї рутини можуть бути передумовою наступної за нею, як в In (sqrt (х)).
Забезпечивши умова х gt; = 0, вводити перевірку аргументу In вже немає необхідності. За визначенням, sqrt повинна повернути ненегативний результат.
Інша перевага контракту полягає в тому, що не доведеться шукати винного в разі порушення перед- або постумови. Якщо порушено передумова, значить, клієнт не забезпечив його виконання і помилка - в коді клієнта. Якщо порушено постусловіем, значить, постачальник не виконав своїх зобов'язань і помилка -в коді постачальника. У будь-якому випадку при таких порушеннях буде порушена виняткова ситуація. Однак тут є якась тонкість.
Якщо порушується передумова, то виняткова ситуація збуджується в тілі клієнта, оскільки постачальник ніяк не може вплинути на передані йому аргументи і загальний стан системи перед зверненням до нього. Якщо ж порушується постусловіем, то виняткова ситуація збуджується в тілі постачальника, оскільки, можливо, він має додаткову інформацію про те, як обробити цю ситуацію або навіть відновити нормальний стан і спробувати все ж завершити свою роботу, використавши, наприклад, інший алгоритм.
Однак не слід думати, що затвердження (до них і ставляться перед-і постумови) можуть використовуватися як засоби обробки спеціальних випадків. Наступний фрагмент коду можна вважати бажаної, але недосяжною метою: read_user_input is
-- Зчитувати вхідні дані до тих пір, - поки вони не будуть вірно введені do
-- зчитування даних ensure valid_input - постусловіем: дані - введені вірно rescue - обробник виняткової ситуації retry - повторити виконання тіла - поточної процедури end
Начебто все повинно працювати як треба: дані зчитуються, перевіряється постусловіем, якщо воно не виконується, то порушується виняткова ситуація, обробник виняткової ситуації починає виконання тіла процедури спочатку. Вихід з цього неявного циклу відбувається тільки тоді, коли дані введені вірно. Але того ж самого ефекту можна добитися за використанням умовних інструкцій і інструкцій циклу. Тому твердження не можна розглядати як засоби організації потоку управління в програмі. Порушення будь-якого затвердження - сигнал про наявність помилки в програмі. Більш точно, порушення передумови - сигнал про помилку в клієнті, порушення постумови - сигнал про помилку в постачальника.
Зауважимо, що передумови і постумови відносяться до інтерфейсу, а не до реалізації. Дійсно, це необхідно, щоб користувач-клієнт знав, як використовувати ту чи іншу властивість класу і що від нього чекати. Це йому необхідно нітрохи не менше, ніж інформація про ім'я властивості, його тип, кількість аргументів і їх типах, словесному описі властивості. Для цієї мети в мові Ейфель введено поняття короткої форми класу, де опущені всі деталі реалізації і неекспортіруемие властивості класу. В опису же всіх інших властивостей входять і передумови, і постумови. Коротка форма класу породжується за допомогою спеціальних утиліт з вихідних текстів і служить документацією для інших розробників.
6. Твердження про властивості об'єкта
Часто доводиться мати справу з об'єктами, які на протязі всього свого життєвого циклу зберігають деякі властивості незмінними. Візьмемо двусвязний список (для простоти вказані тільки атрибути класу): class BILINKED_LIST feature - Доступ до сусідніх елементів next: BILINKED_LIST - наступний елемент prev: BILINKED_LIST - попередній елемент end - class BILINKED_LIST
Для будь-яких двох вузлів х і у таких, що х. next = y, буде також виконано y.prev = x. І це властивість зберігається протягом усього часу життя двусвязного списку. Щоб висловити це властивість, існує відповідне твердження під назвою «інваріант класу». У ньому описуються ті умови, які повинні бути істинними завжди. Після додавання секції invariant текст класу буде виглядати наступним чином: class BIL.INKED_L.IST feature - Доступ до сусідніх елементів next: BILINKED_LIST - наступний елемент prev: BILINKED_LIST - попередній елемент invariant consistent_next: next / = Void implies next.prev = Current consistent_prev: prev / = Void implies prev.next = Current end - class BILINKED_LIST
Тут Current посилається на поточний об'єкт (синонім this в Java і С ++).
Оскільки інваріант класу повинен бути завжди істинним, він перевіряється і до звернення до властивості постачальника, і після нього. Підсумовуючи все вищесказане, отримуємо наступну схему (тим, хто знайомий з трійками Хоара, вона здасться вельми схожою на них):
To є перед виконанням тіла рутини повинні бути виконані інваріант класу і передумова даної рутини. Після виконання тіла рутини повинні бути виконані постусловіем даної рутини і інваріант класу.
Таким чином, щоб після виконання тіла рутини інваріант класу був виконаний, він повинен бути виконаний до її виконання. Тобто інваріант повинен бути виконаний і до виконання тіла попередньої рутини, а значить, і до виконання попередньої по відношенню до попередньої і т. Д. Де ж цей ланцюжок закінчується? Для відповіді на це питання розглянемо проблему з іншого боку. Яка рутина виконується першою? Звичайно, процедура створення об'єкта (конструктор).
Якраз перед її викликом об'єкт ще не створений, і ні про яке инварианте класу мови бути не може. Насправді процедура створення має дещо іншу схему коректності:
Тут DEFAULT означає стан об'єкта відразу після ініціалізації, але ще до виконання процедури створення (наприклад, в Ейфелі в цьому стані всі атрибути об'єкта обнулені). З вищесказаного можна зробити чудовий висновок про роль процедури створення об'єкта: вона забезпечує виконання інваріанта класу. Всі інші властивості об'єкта знаходяться в більш вигідному становищі: їм всього лише доводиться підтримувати цей стан.
До сих пір розглядалися приклади завдання контрактів без урахування ієрархічної структури успадкування класів. При наявності такої структури все стає трохи цікавіше. Спочатку звернемося до інваріанта класу. Припустимо, що замість простого списку нам потрібно відсортоване. Можлива реалізація приведена нижче: class SORTED_LIST inehrit
BILINKED_LIST - Список є двусвязного COMPARABLE - Елементи списку відсортовані invariant prev_is_less:
-- Попередній елемент не більше поточного prev / = Void implies prev lt; = Current next_is_greater:
-- Наступний елемент не менше поточного next / = Void implies next gt; = Current end - class S0RTED_LIST
Очевидно, що і клієнт класу BILINKED_LIST, і рутини, які успадковуються з BILINKED_LIST, має право розраховувати на те, що додавання нащадка до BILINKED_LIST ніяк не відіб'ється на них (вони навіть можуть і не знати про такий нащадку). Тому інваріант класу насправді є об'єднанням по «І» безпосереднього інваріанта і інваріантів всіх його предків. В результаті нащадок не може зруйнувати контракти предка.
Виходячи з цього ж принципу будуються перед- і постумови. Звернемося до іншого прикладу. Нехай потрібно реалізувати клас для сортування масиву. Найпростіший сортувальник, який дозволяє сортувати тільки масиви з попарно різними елементами, може виглядати так: class SIMPLE_S0RTER [G -gt; COMPARABLE] feature - Сортування sort (data: ARRAY [G]) is
-- Відсортувати масив data no - зростанню require non_void_data: data / = Void - масив існує different_elements: all_different (data) - все елементи масиву різні ensure sorted_data: is_sorted (data) - на виході масив відсортований end - class SIMPLE_S0RTER
Клієнт може використовувати змінну sorter типу SIPLE_S0RTER для сортування своїх даних: sorter.sort (my_data)
Оскільки клієнт «не знає» динамічного типу змінної sorter, то він може задовольнити тільки ті передумови, які оголошені в класі SIMPLE_SORTER. Отже, будь-яка зміна контракту в передумовах може лише «спростити» їх, зробити більш м'якими. Таким чином, передумови при перевизначенні властивості класу об'єднуються за допомогою операції «АБО». Щоб підкреслити це, до ключового слова require додається слово else. З іншого боку, клієнт може розраховувати, що постусловіем буде виконано незалежно від динамічного типу sorter. Отже, постумови, як і інваріанти, повинні об'єднуватися з «І». У цьому випадку після ensure додається then. Наприклад, клас, який вже дозволяє сортувати масиви з повторюваними елементами, якщо вони не рівні Void, і гарантує, що сортування буде стабільною, може виглядати так: class ROBUST.SORTER [G -gt; COMPARABLE] inherit
SIMPLE_SORTER redefine sort - процедура sort переопределяется - в цьому класі end feature sort (data: ARRAY [G]) is
-- Відсортувати масив data --по зростанню require else non_void_data: data / = Void - масив існує non_void_elements: not has (data, Void) - в ньому немає порожніх елементів ensure then stable_data: is_stable (old clone (data), data) - - сортування стабільна end - class R0BUST_S0RTER
Повний передумова процедури sort в класі R0BUST_S0RTER таке:
(Data / = Void and thea all_different (data)) or else (data / = Void and then not has (data, Void))
А ось її постусловіем (конструкція old дозволяє посилатися на значення стоїть після неї вираження, обчислене до виконання процедури): is_sorted (data) and then is_stable (old clone (data), data)
Інший аспект використання тверджень полягає в тому, яку ціну доводиться за них платити при виконанні програми. Адже розмір програми зростає, а швидкість виконання падає, причому, можливо, має велике значення. Відповідь проста: при випуску програма компілюється так, що ніякі твердження не включаються в об'єктний модуль. Твердження актуальні тільки на час налагодження та як засіб самодокументірованія. Їх порушення -сигнал про помилку в програмі. Коли налагодження закінчена, жодного порушення твердження не відбувається, а оскільки твердження не мають (точніше сказати, не повинні мати) побічних ефектів, то виключення їх з програми ніяк не впливає на її функціонування.