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

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

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

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

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

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

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


Комп'ютер Це незавершена стаття про комп'ютери.
Ви можете допомогти проекту, виправивши або дописавши її.