Project F@BOOL@ is aimed to development of a transparent, compact, and
portable verifying compiler. It is assumed that F@BOOL@ will exploit efficient
decision procedures for validation of correctness conditions (instead of semiautomatic
theorem provers). In particular, F@BOOL@ will extensively use
SAT-solvers for validation of Boolean encoding of correctness conditions. The
target group of F@BOOL@ users comprises Computer Science, Information
Technology and Mathematics students willing to comprehend program verification.
The technical report is the second part of F@BOOL@ documentation. It
presents informal introduction to Floyd-style verification of program, formal
syntax, static and run-time semantics of Logical Annotations for a toy
programming language Mini-NIL. (This language is a prototype of F@BOOL@
virtual machine.)