Формальна верифікація: відмінності між версіями
| [перевірена версія] | [перевірена версія] |
Вилучено вміст Додано вміст
Hjvfy (обговорення | внесок) |
стильові правлення, правопис |
||
Рядок 3:
'''Верифіка́ція форма́льна''' — в [[інформаційні технології|інформаційних технологіях]], [[доказ]], або [[заперечення]] [[Бієкція|відповідності]] системи у відношенні до певної [[формальна специфікація|формальної специфікації]] або характеристики, із використанням [[формальні методи|формальних методів]] [[математика|математики]].
==Обґрунтування==
Тестування програмного забезпечення не може довести, що система, алгоритм або програма не містить ніяких помилок і дефектів та задовольняє певним властивостям. Це може зробити формальна верифікація.
Рядок 12:
Верифікація являє собою формальний доказ на абстрактній математичній моделі системи, в припущенні про те, що відповідність між математичною моделлю і природою системи вважається заданим. Наприклад, щодо побудованої моделі або математичного аналізу, доказ правильності алгоритмів і програм.
Прикладами математичних об'єктів, часто використовуваних для моделювання та формальної верифікації програм і систем, є:
*формальна семантика мов програмування, наприклад операційна семантика, денотаціонная семантика, аксіоматична семантика ([[Логіка Гоара]]), [математична семантика програм].
Рядок 38:
==Автоматична перевірка доказу==
Доказ може бути автоматизований повністю лише для дуже невеликого кола простих теорій, тому
Для підтримки строгості при перевірці доказу верифікатором слід перевірити ще й верифікатор, для чого потрібен ще один верифікатор і так далі. Отриманий нескінченний ланцюг верифікаторів можна було б згорнути, побудувавши веріфікуючий себе верифікатор, що володіє здатністю розвернутися до застосовного на практиці.
| |||