maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State Universitymais-1057Research ArticleОригинальные статьиArticlesПример верификации в проекте F@BOOL@, основанном на булевских решателяхF@BOOL@: experiment with a simple verifying compiler based on SAT-solversШиловН. В.ShilovN. V.shilov@iis.nsk.suИнститут систем информатики им. А.П. Ершова СО РАН, Новосибирский государственный университет и Новосибирский государственный технический университетRussian Federation201020122010174111124Copyright © Шилов Н.В., 20102010Шилов Н.В.Shilov N.V.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1057

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

A verifying compiler is a system computer program that translates programs written by man from a high-level language into equivalent executable programs, and besides, proves (veri¯es) mathematical statements speci¯ed by man about the properties of the programs being translated. The purpose of the F@BOOL@ project is to develop a transparent for users, compact and portable verifying compiler F@BOOL@ for anno- tated computational programs, that uses e®ective and sound automatic SAT-solvers (i.e. programs that check satis¯ability of prepositional Boolean formulas in the conjunctive normal form) as means of automatic validation of correctness conditions (instead of semi-automatic proof techniques). The key idea is Boolean representation of all data instead of Boolean abstraction or ¯rst-order representation. (It makes di®erence be- tween F@BOOL@ and SLAM.) Our project is aimed at the veri¯cation of functional properties, and it assumes generation of ¯rst-order veri¯cation conditions (from invari- ants), and the validation/refutation of each veri¯cation condition using SAT-solvers after \conservative" translation of the veri¯cation conditions into Boolean form. During the period from 2006 to 2009, a popular (at that time) SAT-solver zCha® was used in the F@BOOL@ project. The ¯rst three veri¯cation experiments that have been exercised with its help are listed below: swapping values of two variables, checking whether three input values are lengths of sides of an equilateral or isosceles triangle, and detecting a unique fake in a set of 15 coins. The paper presents general outlines of the project and details of the last (the most extensive) experiment.

формальная верификация программоперационная и трансформационная семантика программметод верификации Флойда - Хоараусловия корректностибулевские решателиformal program veri¯cationoperational and transformational semanticsFloydHoare proof techniquecorrectness conditionsSAT-solversReferencesАхо А., Хопкрофт Дж., Ульман Дж. Построение и анализ вычислительных алгоритмов. М.: Мир. 1979.Ахо А., Хопкрофт Дж., Ульман Дж. Построение и анализ вычислительных алгоритмов. М.: Мир. 1979.Бодин Е.В., Калинина Н.А., Шилов Н.В. Проект верифицирующего компилятора F@BOOL@ Часть I: Общее описание проекта F@BOOL@, его место в компонентном подходе к программированию. Язык Mini-NIL - прототип языка виртуальной машины проекта. Препринт №131 Института систем информатики им. А.П. Ершова СО РАН, 2005.Бодин Е.В., Калинина Н.А., Шилов Н.В. Проект верифицирующего компилятора F@BOOL@ Часть I: Общее описание проекта F@BOOL@, его место в компонентном подходе к программированию. Язык Mini-NIL - прототип языка виртуальной машины проекта. Препринт №131 Института систем информатики им. А.П. Ершова СО РАН, 2005.Бодин Е.В., Калинина Н.А., Шилов Н.В. Проект верифицирующего компилятора F@BOOL@. Часть II: Логические аннотации в языке Mini-NIL, их статическая семантика и семантика времени исполнения. Препринт №138 Института систем информатики им. А.П. Ершова СО РАН, 2006.Бодин Е.В., Калинина Н.А., Шилов Н.В. Проект верифицирующего компилятора F@BOOL@. Часть II: Логические аннотации в языке Mini-NIL, их статическая семантика и семантика времени исполнения. Препринт №138 Института систем информатики им. А.П. Ершова СО РАН, 2006.Дейкстра В.Э. Дисциплина программирования. М.: Мир, 1978.Дейкстра В.Э. Дисциплина программирования. М.: Мир, 1978.Грис Д. Наука программирования. М.: Мир, 1984.Грис Д. Наука программирования. М.: Мир, 1984.Шилов Н.В., Бодин Е.В. Ии И. О программных логиках - просто // Системная информатика, выпуск 8. Новосибирск: Наука, 2002. С. 206-249.Шилов Н.В., Бодин Е.В. Ии И. О программных логиках - просто // Системная информатика, выпуск 8. Новосибирск: Наука, 2002. С. 206-249.Шилов Н.В., Ануреев И.С., Бодин Е.В. О генерации условий корректности для императивных программ // Программирование. 2008, №6. С. 1-20.Шилов Н.В., Ануреев И.С., Бодин Е.В. О генерации условий корректности для императивных программ // Программирование. 2008, №6. С. 1-20.Шилов Н.В. Заметки о трёх парадигмах программирования // Компьютерные инструменты в образовании. 2010, №2. С. 24-37.Шилов Н.В. Заметки о трёх парадигмах программирования // Компьютерные инструменты в образовании. 2010, №2. С. 24-37.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.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.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.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.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.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.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.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.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.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.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.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.

The authors declare that there are no conflicts of interest present.