Пример верификации в проекте F@BOOL@, основанном на булевских решателях

Верифицирующий компилятор – это системная компьютерная программа, которая транслирует написанные человеком программы с языка высокого уровня в эквивалентные исполнимые программы и, кроме того, доказывает (верифицирует) специфицированные человеком математические утверждения о свойствах транслируемых программ. Цель проекта F@BOOL@ – разработка понятного для пользователей, компактного и переносимого верифицирующего компилятора аннотированных вычислительных программ, использующего эффективные и достоверные автоматические SAT-решатели в качестве средств автоматической проверки истинности условий корректности (вместо средств полуавтоматического доказательства). В период с 2006 по 2009 гг. в проекте F@BOOL@ использовался SAT-решатель zChaff. С его помощью были выполнены первые эксперименты по верификации простых программ на Mini-NIL: программы обмена переменных своими значениями, проверки троек целых чисел быть длинами сторон равностороннего или равнобедренного треугольника, и поиска одной фальшивой среди 15 монет с использованием чашечных весов. В работе рассказано об основных идеях проекта F@BOOL@ и приведены детали эксперимента по верификации программы, решающей головоломку о монетах.