Fabulous arrays I: Operational and transformational semantics of static arrays in verification project F@BOOL@

The purpose of the F@BOOL@ project is to develop a transparent for users, compact, portable and extensible verifying compiler F@BOOL@ for annotated computer programs, that uses effective and sound automatic programs for checking satisfiability of propositional Boolean formulas. The kernel programming language of the project interprets all variables by residuals modulo some fixed integer (that is a parameter). Paper presents an extension of the kernel language by different variable ranges and static multi-dimensional arrays, provides two kinds of semantics of the extension | operational and transformational (into the kernel language), sketches manual correctness proof for the transformational semantics.