Верифицирующий компилятор - это системная компьютерная программа, которая транслирует написанные человеком программы с языка высокого уровня в эквивалентные исполнимые программы, и кроме того, доказывает (верифицирует) специфицированные человеком математические утверждения о свойствах транслируемых программ. Работа представляет общее описание проекта верифицирующего компилятора F@BOOL@, дает теоретическое обоснование его реализуемости, методическую проработку его места и роли в компонентном (сборочном) подходе к созданию больших программных систем.
Кроме того, работа фиксирует формальный синтаксис и операционную семантику модельного и учебного языка программирования Mini-NIL, который является прототипом языка виртуальной машины проекта F@BOOL@, на котором будут апробированы основные идеи системы F@BOOL@. Вынесенное в название работы указание "Часть I" подразумевает, что данная публикация является первой частью документации по проекту F@BOOL@ и что по мере проработки проекта будет опубликованы следующие части документации.
Работа поддержана грантом РФФИ № 05-07-90162.