Для верификации программ придумано множество различных методик. В том числе, например, "верификация на модели" (model checking), когда верифицируется не сам код программы, а его модель (обычно некая система переходов или автомат специального вида). На таких моделях успешно проверяется выполнение ряда свойств (например, отсутствие взаимоблокировок, дедлоков, в мультипроцессном коде).
Но почему бы не посмотреть на верификацию спецификаций? Ведь для спецификаций тоже можно формулировать свойства и проверять их! Задача состоит в определении таких свойств и предложению методов верификации спецификаций на выполнение этих свойств.
Сложность:
постановка задачи (непонятно, что это за свойства, о каких спецификациях идет речь)
вычислительная сложность (как и любая верификация)
Комментариев нет:
Отправить комментарий