Contract Strengthening through Constrained Horn Clause Verification

Emanuele De Angelis
(IASI-CNR, Italy)
Fabio Fioravanti
(DEc, University of Chieti-Pescara, Italy)
Alberto Pettorossi
(DICII, University of Rome "Tor Vergata", Italy)
Maurizio Proietti
(IASI-CNR, Italy)

The functional properties of a program are often specified by providing a contract for each of its functions. A contract of a function consists of a pair of formulas, called a precondition and a postcondition, which, respectively, should hold before and after execution of that function. It might be the case that the contracts supplied by the programmer are not adequate to allow a verification system to prove program correctness, that is, to show that for every function, if the precondition holds and the execution of the function terminates, then the postcondition holds. We address this problem by providing a technique which may strengthen the postconditions of the functions, thereby improving the ability of the verifier to show program correctness. Our technique consists of four steps. First, the translation of the given program, which may manipulate algebraic data structures (ADTs), and its contracts into a set of constrained Horn clauses (CHCs) whose satisfiability implies the validity of the given contracts. Then, the derivation, via CHC transformation performed by the VeriCaT tool, of a new set of CHCs that manipulate only basic sorts (such as booleans or integers) and whose satisfiability implies the satisfiability of the original set of clauses. Then, the construction of a model, if any, of the new, derived CHCs using the CHC solver SPACER for basic sorts. Finally, the translation of that model into the formulas that suitably strengthen the postconditions of the given contracts. We will present our technique through an example consisting of a Scala program for reversing lists. Note that the Stainless verifier is not able to prove the correctness of that program when considering the given contracts, while it succeeds when considering the contracts with the strengthened postconditions constructed by applying our technique.

In Geoffrey W. Hamilton, Temesghen Kahsai and Maurizio Proietti: Proceedings 9th Workshop on Horn Clauses for Verification and Synthesis and 10th International Workshop on Verification and Program Transformation (HCVS/VPT 2022), Munich, Germany, 3rd April 2022, Electronic Proceedings in Theoretical Computer Science 373, pp. 23–34.
Published: 22nd November 2022.

ArXived at: https://dx.doi.org/10.4204/EPTCS.373.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org