Формальна специфікація

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до навігації Перейти до пошуку

Форма́льна специфіка́ція — математичний опис програмного забезпечення або обладнання, яке може бути використане для розробки реалізації. В ній описується, що має робити система, але не (обов'язково) вказується як. Маючи таку специфікацію, можна, використовуючи техніку формальної верифікації продемонструвати, що запропонований проєкт системи є правильним, по відношенню до специфікації. Такий підхід має перевагу в тому, що запропоновані невірні проєкти систем можуть бути переглянуті до того як буде зроблено основні витрати на власне саму реалізацію. Альтернативний підхід полягає в тому, аби, виконуючи кроки по уточненню специфікації, вірність яких можна довести, перетворити специфікацію на реалізацію, яка буде вірною через побудову.

Важливо зазначити, що проєкт (або реалізацію) ніколи не можна вважати «вірним» окремо, але, лише «вірним по відношенню до вказаної специфікації».

Джерела інформації[ред. | ред. код]

Див. також[ред. | ред. код]

Література[ред. | ред. код]