На мой взгляд, в русскоязычном секторе интернета тематика формальной верификации освещена недостаточно, и особенно не хватает простых и наглядных примеров.
Я приведу такой пример из зарубежного источника, и дополню собственным решением известной задачи о переправе волка, козы и капусты на другую сторону реки.
Но вначале вкратце опишу, что из себя представляет формальная верификация и зачем она нужна.
Под формальной верификацией обычно понимают проверку одной программы либо алгоритма с помощью другой.
Это нужно для того, чтобы удостовериться, что поведение программы соответствует ожидаемому, а также обеспечить её безопасность.
Формальная верификация является самым мощным средством поиска и устранения уязвимостей: она позволяет найти все существующие дыры и баги в программе, либо же доказать, что их нет.
Стоит заметить, что в некоторых случаях это бывает невозможно, как например, в задаче о 8 ферзях с шириной доски 1000 клеток: всё упирается в алгоритмическую сложность либо проблему остановки.
Однако в любом случае будет получен один из трёх ответов: программа корректна, некорректна, или же — вычислить ответ не удалось.
В случае невозможности нахождения ответа, зачастую можно переработать неясные места программы, уменьшив их алгоритмическую сложность, для того чтобы получить конкретный ответ да либо нет.
А применяется формальная верификация, например, в ядре Windows и операционных системах беспилотников Darpa, для обеспечения максимального уровня защиты.
Мы будем использовать Z3Prover, очень мощный инструмент для автоматизированного доказательства теорем и решения уравнения.
Причём Z3 именно решает уравнения, а не подбирает их значения грубым брутфорсом.
Это означает, что он способен находить ответ, даже в случаях когда комбинаций входных вариантов и 10^100.
А ведь это всего лишь около дюжины входных аргументов типа Integer, и подобное зачастую встречается на практике.
Задача о 8 ферзях (Взята из англоязычного мануала).
Читать полностью »
