Проєктування за контрактом

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

Проєктування за контрактом (англ. design by contract (DbC), programming by contract, contract-based programming) — методологія розробки програмного забезпечення. Вона вимагає від проєктувальників задавати формальні, точні та такі, що підлягають верифікації, специфікації інтерфейсів програмних компонентів. Окрім задання абстрактних типів даних вимагається також задання передумов, післяумов та інваріантів. Такі специфікації називаються «контрактами» згідно з концептуальною метафорою умов і зобов'язань у бізнесових контрактах.

Проєктування модуля за контрактом

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

Історія

ред.

Термін був запропонований Бертраном Меєром під час розробки мови Eiffel і описаний в кількох статтях, починаючи з 1986 року, зокрема в статті Design by Contract [1] та двох виданнях його відомої книги Object-Oriented Software Construction [Архівовано 2 лютого 2017 у Wayback Machine.]. Проєктування за контрактом засноване на працях з формальної специфікації, формальної верифікації та логіці Гоара.

Контрактне програмування дає чітку концепцію керування процесом проєктування і передбачає:

  • використання успадкування та динамічного зв'язування;
  • використання обробки винятків;
  • можливість автоматичного документування програмного забезпечення.

Опис

ред.

Основна ідея контрактного програмування — модель взаємодії елементів програмної системи на основі взаємних зобов'язань та вигод. Це метафора із бізнесу, де «клієнт» та «постачальник» укладають «контракт», що описує наступну поведінку:

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

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

В об'єктно-орієнтованому програмуванні контракт методу зазвичай містить:

  • вхідні типи даних та їхні можливі значення;
  • тип результату та його можливі значення;
  • умови виникнення винятків, їхні типи та можливі значення;
  • передумови (їх можна послабити, але не посилити в підкласі);
  • післяумови (їх можна посилити, але не послабити в підкласі);
  • інваріанти;
  • побічні ефекти;
  • гарантії обмеження споживання ресурсів (часу чи пам'яті).

Контрактне програмування дозволяє підвищити повторне використання коду, оскільки зобов'язання модуля чітко виписані. Контракт модуля можна розглядати як один із способів документування ПЗ.

Підтримка DbC мовами програмування

ред.

Мови програмування з нативною підтримкою

ред.

Мови, які включають більшість рис DbC:

Мови програмування з підтримкою DbC за допомогою сторонніх бібліотек

ред.

Для мов без нативної підтримки DbC розроблені різні бібліотеки, препроцесори та інші інструменти:

  • Ada, через GNAT pragmas для передумов та післяумов
  • C та C++, через препроцесор DBC for C, GNU Nana, бібліотеку Contract++, компілятор C++ Digital Mars. Бібліотека Loki надає механізм ContractChecker на відповідність класу DbC
  • C# (та інші мови .NET), через Code Contracts (проєкт Microsoft Research, інтегрований в .NET Framework 4.0)
  • Groovy, через GContracts
  • Java, через OVal з AspectJ, Contracts for Java (Cofoja), Java Modeling Language (JML), Bean Validation (лише пре- та післяумови), valid4j
  • JavaScript, через AspectJS (особливо AJS_Validator), Cerny.js, ecmaDebug, jsContract, jscategory
  • Common Lisp, через макроси або протокол метаоб'єктів CLOS
  • Nemerle, через макроси
  • Perl, через CPAN-модулі Class::Contract (Damian Conway) або Carp::Datum (Raphael Manfredi)
  • PHP, через PhpDeal, Praspel або ContractLib (Stuart Herbert's)
  • Python, через пакети PyContracts, Decontractors, dpcontracts, zope.interface, PyDBC або Contracts for Python
  • Ruby, через DesignByContract (Brian McCallister), Ruby DBC, ruby-contract або contracts.ruby
  • Rust, через бібліотеку Hoare

Література

ред.
  • Mitchell, Richard, and McKim, Jim: Design by Contract: by example, Addison-Wesley, 2002.
  • Meyer, Bertrand Object-Oriented Software Construction, 2nd Edition, Prentice Hall, 1997.

Примітки

ред.
  1. Meyer, Bertrand: Applying "Design by Contract", in Computer (IEEE), 25, 10, October 1992, pp. 40–51, також доступна online [Архівовано 21 вересня 2017 у Wayback Machine.]