Мал. 4. Процес формальних перетворень

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

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

Найбільш відомим прикладом методу формальних перетворень є метод "чистої кімнати" (Cleanroom), розроблений компанією IBM [239, 310, 219, 284]. Цей метод передбачає покрокову розробку ПЗ, коли на кожному кроці застосовується формальні перетворення. Це дозволяє відмовитися від тестування окремих програмних модулів, а тестування всієї системи відбувається після її збірки. Цей підхід більш докладно розглянуто в главі 19.

Як метод "чистої кімнати", так і інші методи формальних перетворень ґрунтуються на В-методі [348]. Всі ці методи мають кілька "вроджених" недоліків, а вартість розробки ПЗ за допомогою цих методів не набагато відрізняється від вартості розробок іншими методами. Методи формальних перетворень зазвичай застосовують для розробки систем, які повинні задовольняти суворим вимогам надійності, безвідмовності і безпеки, так як вони гарантують відповідність створених систем їх специфікаціям.

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