B-метод
B — загальний термін, яким називають B-Method (формальний метод розробки програмного забезпечення), процес такої розробки, мову запису специфікації, і інструменти що їх підтримують (B-Toolkit)
Історія
Метод розроблений Жаном-Реймондом Абріалем у Великій Британії та Франції.
Використовувався при створенні в Європі систем критичних щодо надійності (помилка в яких створює небезпеку для людей та інших ресурсів). Наприклад 14 лінія паризького метро[1]
Недавно створили ще один метод, названий Event-B. Він розглядається як вдосконалення B (відомого також як класичний B). Event-B має простіший синтаксис, що полегшує його вивчення та використання. Інструменти, що його підтримують, називаються платформою Rodin.
B-Method
B-Method — це набір математичних технологій для специфікації, проектування та реалізації компонент програмного забезпечення. Системи моделюються як сукупності незалежних Абстрактних Машин, для яких на всіх стадіях розробки застосовується об'єктно-орієнтований підхід.
Абстрактна Машина описується з використанням Abstract Machine Notation (AMN). Стандартна нотація використовується на всіх рівнях опису, від специфікації до реалізації.
AMN — мова формальної специфікації, що базується на станах. Вона вийшла з тієї ж школи, що і VDM та Z. Абстрактна машина включає стан разом з операціями на тому стані. У специфікаціях та конструюванні Абстрактної Машини стани моделюються з використанням таких понять як множина, відношення, функція, послідовність та подібних. Оператори моделюються з використанням перед- та післяумов.
У реалізації абстрактної машини стан знову моделюється з використанням теоретико-множинної моделі, але цього разу ми вже маємо реалізацію цієї моделі. Ця операція описується з використанням псевдокоду, який є підмножиною AMN.
Математичний запис
https://web.archive.org/web/20100127025201/http://www.b-core.com/ONLINEDOC/MathsNotation.html