DESIGNING A LIBRARY TO SIMPLIFY PROGRAM VERIFICATION CONDITIONS

Abstract

The ExpLib library described for the equivalent transformation of arithmetic and logical expressions in order to reduce them to the simplest form based on the classical relations of integer arithmetic and mathematical logic. Annotating the program with invariants specified at certain points of the program reduces the problem of program verification to checking the truth of a set of logical expressions. However, the problem of derivability is algorithmically unsolvable even for sufficiently simple subject area, such as elementary arithmetic. Therefore, it is important to develop computer tools that can simplify the task of program verification. It is especially important to have such systems for programming teaching. These include the technology of symbolic execution of programs and tools for equivalent transformation and simplification of symbolic expressions. Formal methods of program verification are reflected in many modern studies. The article describes the technology of automatic equivalent conversion the arithmetic and logical expressions to the simplest standardized form built on the basis of the ExprLib library. These transformations have the property of idempotency, and the equivalent expressions have a single normalized representation. The library is written in the Python algorithmic language using recursion on tree-type data structures. The library is implemented by classes and functions built in Python using lists, sets, and dictionaries. These classes represent trees, monomials and polynomials, relations and their conjunctions, as well as implications. To simplify the implications, the reduction rule of conjunctions is used. The ExpLib is used in the VerPro system for symbolic execution and Python programs verification. To verify the identical truth of the implications, which represent the verification conditions, solvers of the Z3 theorem proving system are used. The VerPro system is experimental and currently limited to integer arithmetic applications. Having the own library allows us to expand the scope of the system. The VerPro system is developing in the direction of invariant generating and expanding the program area.