  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.
