Пример верификации в проекте F@BOOL@, основанном на булевских решателях
Аннотация
Верифицирующий компилятор - это системная компьютерная программа, которая транслирует написанные человеком программы с языка высокого уровня в эквивалентные исполнимые программы и, кроме того, доказывает (верифицирует) специфицированные человеком математические утверждения о свойствах транслируемых программ. Цель проекта F@BOOL@ - разработка понятного для пользователей, компактного и переносимого верифицирующего компилятора аннотированных вычислительных программ, использующего эффективные и достоверные автоматические SAT-решатели в качестве средств автоматической проверки истинности условий корректности (вместо средств полуавтоматического доказательства). В период с 2006 по 2009 гг. в проекте F@BOOL@ использовался SAT-решатель zChaff. С его помощью были выполнены первые эксперименты по верификации простых программ на Mini-NIL: программы обмена переменных своими значениями, проверки троек целых чисел быть длинами сторон равностороннего или равнобедренного треугольника, и поиска одной фальшивой среди 15 монет с использованием чашечных весов. В работе рассказано об основных идеях проекта F@BOOL@ и приведены детали эксперимента по верификации программы, решающей головоломку о монетах.
Ключевые слова
формальная верификация программ, операционная и трансформационная семантика программ,
метод верификации Флойда - Хоара,
условия корректности,
булевские решатели
MSC2020: 519.681+519.682.1
Об авторе
Н. В. Шилов
Институт систем информатики им. А.П. Ершова СО РАН,
Новосибирский государственный университет и Новосибирский государственный технический университет
Россия
Россия
Список литературы
1. Ахо А., Хопкрофт Дж., Ульман Дж. Построение и анализ вычислительных алгоритмов. М.: Мир. 1979.
2. Бодин Е.В., Калинина Н.А., Шилов Н.В. Проект верифицирующего компилятора F@BOOL@ Часть I: Общее описание проекта F@BOOL@, его место в компонентном подходе к программированию. Язык Mini-NIL - прототип языка виртуальной машины проекта. Препринт №131 Института систем информатики им. А.П. Ершова СО РАН, 2005.
3. Бодин Е.В., Калинина Н.А., Шилов Н.В. Проект верифицирующего компилятора F@BOOL@. Часть II: Логические аннотации в языке Mini-NIL, их статическая семантика и семантика времени исполнения. Препринт №138 Института систем информатики им. А.П. Ершова СО РАН, 2006.
4. Дейкстра В.Э. Дисциплина программирования. М.: Мир, 1978.
5. Грис Д. Наука программирования. М.: Мир, 1984.
6. Шилов Н.В., Бодин Е.В. Ии И. О программных логиках - просто // Системная информатика, выпуск 8. Новосибирск: Наука, 2002. С. 206-249.
7. Шилов Н.В., Ануреев И.С., Бодин Е.В. О генерации условий корректности для императивных программ // Программирование. 2008, №6. С. 1-20.
8. Шилов Н.В. Заметки о трёх парадигмах программирования // Компьютерные инструменты в образовании. 2010, №2. С. 24-37.
9. Anureev I.S., Bodin E.V., Gorodnyaya L.V., Marchuk A.G., Murzin F.A., Shilov N.V. On the Problem of Computer Language Classification // Joint NCC&IIS Bulletin, Series Computer Science. 2008. Vol. 28. P. 1-29.
10. Ball T., Cook B., Levin V., and Rajamani S. K. SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft // Springer-Verlag, Berlin, LNCS. 2004. Vol. 2999. P. 1-20.
11. Beyer D., Henzinger T.A., Jhala R., and Majumdar R. The Software Model Checker Blast: Applications to Software Engineering // Int. Journal on Software Tools for Technology Transfer. 2007. N 9. P. 505-525.
12. Floyd R.W. Assigning meanings to programs. Proc. of a Symposium in Applied Mathematics. Mathematical Aspects of Computer Science, Vol. 19. American Math. Society, Providence, R. I., 1967. P. 19-32.
13. Hoare C. A. R. The Verifying Compiler: A Grand Challenge for Computing Research. Perspectives of Systems Informatics (PSI'2003), Springer-Verlag, Berlin, LNCS. Vol. 2890. 2003. P. 1-12.
14. Shilov N.V., Bodin Eu.V, Shilova S.O. Fabulous arrays I: Operational and transformational semantics of static arrays in vericationproject F@BOOL@. Bull. Nov. Comp. Center, Comp. Science. Vol. 29. 2009. P. 121-140.
Рецензия
Для цитирования:
Шилов Н.В. Пример верификации в проекте F@BOOL@, основанном на булевских решателях. Моделирование и анализ информационных систем. 2010;17(4):111-124.
For citation:
Shilov N.V. F@BOOL@: experiment with a simple verifying compiler based on SAT-solvers. Modeling and Analysis of Information Systems. 2010;17(4):111-124. (In Russ.)
Просмотров: 372
Послать статью по эл. почте 