Формальні методи
В інформатиці та інженерії програмного забезпечення формальними методами (англ. formal methods) називається група технік, заснованих на математичному апараті для специфікації, розробки та верифікації програмного та апаратного забезпечення [1] . Використання формальних методів для проектування програмного та апаратного забезпечення обумовлено очікуваннями того, що, як і в інших інженерних галузях, використання математичного аналізу може суттєво підняти надійність систем [2] . У цьому формальні методи досить складні, вимагають спеціальної підготовки, тимчасових і ресурсних вкладень, і навіть нерідко грунтуються не завжди досяжних у реальних умовах припущеннях. Це призводить до того, що формальні методи найчастіше знаходять застосування у проектуванні високоточних систем, де важливість безпеки виправдовує будь-які засоби.
Зміст
Можна виділити три рівні застосування формальних методів:
Розробляється формальна специфікація, потім програмний код пишеться, дивлячись на неї. У цьому випадку прірва між формальною та неформальною частиною залишається бездоказовою, але рішення може бути ефективним з погляду його вартості. Перший рівень Програмний код виводиться з формальної специфікації автоматично, використовуються механізми верифікації, доводяться найкритичніші властивості системи. Цей шлях найчастіше вибирається для високоточних систем. Другий рівень Автоматичні доказники теорем використовуються для виведення повністю формалізованих доказів, що перевіряються автоматично. Підхід потребує об'ємних вкладень та досліджень, але виправдовує себе у найкритичніших частинах складних систем, де помилки неприпустимі (наприклад, у проектуванні інтегральних схем).
Підходидо формальних методів також можна класифікувати аналогічно до формальної семантики мов програмування:
Денотаційна семантика (англ. denotational semantics) Значення системи виражається через частково впорядковані множини, а методи покладаються на добре розроблену теорію навколо них. Обмеження методу — у тому, що кожна система може бути інтуїтивно чи природно розглянута як функція. p align="justify"> Операційна семантика (англ. operational semantics) Значення системи позначається послідовністю дій в рамках більш простої обчислювальної моделі (наприклад, лямбда-обчислення або мереж Петрі). Методи славляться своєю простотою, якщо не акцентувати увагу на тому, що вони покладаються на семантику «простішої» системи, яку теж треба через щось визначати. Аксіоматична семантика (англ. axiomatic semantics) Сенс системи визначається термінах передумов і постумов, що дозволяє пов'язати теорію з класичною логікою, але не дає уявлення про те, що конкретно відбувається всередині системи (як досягаються постумови на основі передумов).
Крім того, нерідко різко позитивних результатів можна досягти, пожертвувавши глобальною застосовністю та надформалізацією — такі випадки називають «полегшеними» (lightweight) формальними методами. Їх можна розділити на два типи: з посиленою та з ослабленою автоматизацією. Приклад посиленої автоматизації - аналізатор специфікацій Alloy Analyzer, який для того, щоб звести завдання пошуку моделі до розв'язуваної, звужуючи область пошуку (в результаті Алл працює повністю автоматизовано, на відміну від інтерактивних доказників, але має шанс не знайти деякі проблеми). Приклад ослабленої — збіжність граматик, у якій нерозв'язність задачі еквівалентності двох формальних мов обходитьсятим, що перетворення робить сама людина, а висновки робляться вже за властивостями використаних нею операторів.
Формальні методи застосовуються на різних етапах розробки програмного забезпечення:
Специфікація За допомогою формальних методів можна описати майбутню систему з будь-яким рівнем деталізації. Такий формальний опис може безпосередньо або опосередковано користуватися на більш пізніх етапах. При цьому робота за доказом ряду необхідних функціональних властивостей може починатися відразу і йти паралельно з написанням чи генерацією коду. Існує ціла низка мов та обчислень для формальних специфікацій, але жоден не може претендувати на звання універсального, як Форма Бекуса - Наура для специфікації синтаксису. Розробка Якщо формальна специфікація використовує операційну семантику, поведінка конкретної системи, що спостерігається, можна порівнювати з очікуваним, тому що така семантика може бути здійсненною, а може навіть використовуватися для автоматичного генерування коду. Якщо використовується аксіоматична семантика, то передумови та постумови можуть безпосередньо відобразитись у затвердження у здійснюваному коді. Верифікація Коли формальна специфікація підготовлена, її можна використовуватиме докази потрібних властивостей. Верифікація буває дедуктивною та модельною: дедуктивна використовує автоматичний доказ теорем або специфічні алгебри, а модельна засновує свої висновки не на самій системі, а на побудованій за нею моделі [4] . При цьому модель зовсім не обов'язково будувати вручну, якщо застосовні виявляються техніки на зразок програмного перерізу (англ.).
Докази вручну вимагають серйозних вкладень ресурсів та не дають жодної вигоди, крім підтвердження правильності. В результаті формальні методи використовуютьсяабо в тих областях, де докази можна отримати автоматично програмним шляхом, або в тих, де ціна помилки надто висока (наприклад, при створенні космічних апаратів або магнітно-резонансних томографів).