Journal "Software Engineering"
a journal on theoretical and applied science and technology
ISSN 2220-3397

Issue N3 2021 year

DOI: 10.17587/prin.12.127-139
Applying Program Transformations for Deductive Verification of the List Reverse Program
V. I. Shelekhov, vshel@iis.nsk.su, A. P. Ershov Institute of Informatics Systems, Novosibirsk, 630090, Russian Federation
Corresponding author: Shelekhov Vlaimir I., Head of Laboratory. A. P. Ershov Institute of Informatics Systems, Novosibirsk, 630090, Russian Federation, E-mail: vshel@iis.nsk.su
Received on December 16, 2020
Accepted on February 01, 2021

The program transformation methods to simplify the deductive verification of programs with recursive data types are investigated. The list reversion program is considered as an example. A source program in the C language is translated to the cP functional language which includes no pointers. The resulting program is translated further to the WhyML language to perform deductive verification of the program. The cP language includes the same constructs of the C language except pointers. In the C program, all actions that include pointers are replaced by the equivalent fragments without pointers. These replacement are performed by the special transformations using the results of the program dataflow analysis. Three variants of deductive verification of the transformed list reverse program in the Why3 verification platform with SMT solvers (Z3 4.8.6, CVC3 2.4.1, CVC4 1.7) are performed. First, the recursive WhyML program supplied with specifications was automatically verified successfully using only SMT solvers. Second, the recursive program was translated to the P predicate language. Correctness formulae were constructed for the P program and translated further to the why3 specification language. The formulae proving correctness were easy like the first variant. But correctness formulae for the first and second variants were different. Third, the "imperative" WhyML program that included while loop with additional invariant specifications was verified. The proving was easy but not automatic. So, for deductive verification, recursive program variant appears to be more preferable against imperative program variant.

Keywords: deductive verification, program transformation, functional program, predicate program, algebraic data type, linked list, Linux operating system
pp. 127–139
For citation:
Shelekhov V. I. Applying Program Transformations for Deductive Verification of the List Reverse Program, Programmnaya Ingeneria, 2021, vol. 12, no. 3, pp. 127—139