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

Матеріал з Вікіпедії — вільної енциклопедії.
Jump to navigation Jump to search

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

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

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

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

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