{'fraction_non_alphanumeric': 0.04202782431349698, 'fraction_numerical': 0.007283851700779372, 'mean_word_length': 4.772335505570738, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 24, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Contract Strengthening through Constrained Horn Clause Verification

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.


Introduction
In many program verification techniques à la Floyd-Hoare [11,16], the meaning of a program is specified by providing a contract, that is, a pair of a precondition and a postcondition formula for each of the program functions. A program function is said to be partially correct with respect to a given contract if the precondition holds before function execution, and the function terminates, then the postcondition holds. A program function is said to be totally correct if it is partially correct and it terminates whenever its precondition holds. Many programming languages (for instance, Ada [3], Ciao [15], Eiffel [22], Scala [24], and Solidity [26]) provide support for contract specification.
Programmers write contracts to specify invariant properties of entire programs or program fragments (such as functions, methods, and loops) and these contracts may be used by verifiers (e.g., BOOGIE [1], LEON [27], WHY3 [10], DAFNY [20], and STAINLESS [14]) to generate and possibly prove suitable verification conditions, that is, formulas whose validity guarantees program correctness.
Verification conditions are usually proved by using theorem provers or Satisfiability Modulo Theory (SMT) solvers [2,4,17,23] and constrained Horn clause (CHC) solvers, such as Eldarica [17] and SPACER [18]. In these solvers there is support for a wide range of logical theories, including basic data types, such as integers and booleans, and also more complex data structures.
In the case of programs manipulating complex data structures, such as Algebraic Data Types (ADTs), loop invariants and contracts may be quite complicated and their verification may require the enhancement of the solvers by incorporating inductive proof rules [25,28,29], or tree automata-based techniques [19], or CHC abstractions [12].
Besides the presence of ADTs, there is often one additional reason that makes it difficult to prove the validity of the contracts when using an automated verification system. It is the fact that the contracts specified by the programmer are not sufficiently detailed in specifying the behaviour of the functions.
In order to clarify this point, let us consider the case of a program made out of some functions which may call each other, possibly in a mutually recursive way. Each of these functions has its own contract. Now it may happen that a program verifier is able to prove the contract of a particular function, say g, while it fails to prove the contract of another function, say f , because f calls g and the contract that has been proved for g is not detailed enough. This may happen because the programmer, when specifying contracts, did not take into account the fact that g is called by f, and for the proof of the contract of f a stronger, more detailed contract for g is indeed required. Moreover, these contract interdependencies are not always easy to take into account by the programmer, and this happens in particular when the program is made out of many function definitions.
In this paper we present a novel technique for strengthening the function contracts in the case of programs that manipulate ADTs, and then, our technique allows an easier proof of contract correctness. Our technique consists of four steps.
Step (i): First, we translate the given program with its contracts into a set of CHCs, so that the contract verification problem is translated into an equivalent satisfiability problem for that set of CHCs.
Step (ii): Then, by using already known methods [6,7], we transform this set of CHCs into a new set where all ADT terms are removed. In particular, we use the VeriCaT tool [9]. These methods are sound, in the sense that the satisfiability of the transformed clauses implies the satisfiability of the original set of clauses. Under suitable hypotheses, these methods are also complete, that is, the original and the transformed set of clauses are equisatisfiable [8]. In this way, we separate the concern of dealing with ADTs (at transformation time) from the concern of dealing with simpler, non-inductive constraint theories (at solving time), thus avoiding the complex interaction between inductive reasoning and constraint solving. Usually, during this transformation new predicate symbols are introduced in the derived CHCs.
Step (iii): Then, we invoke a CHC solver (in our case SPACER) to show the satisfiability of the new, transformed set of CHCs and to construct the models, if any, of the new predicates which have been introduced.
Step (iv): Finally, from those models we construct the formulas which strengthen the given contracts.
The viability and the power of this novel technique will be shown in the following sections through a simple example dealing with lists.

Verification of Program Contracts
In this section we present the program verification problem we consider with the help of an example. Let us consider the Scala program Reverse, depicted in Figure 1, for computing the reversal of a list. In that program the function preconditions and postconditions are specified by require and ensuring assertions, respectively. The contract for the function rev states that, if a list l of integers is sorted in ascending order (w.r.t. ≤), then the list rev(l) is sorted in descending order (that is, it is sorted w.r.t. ≥). The ascending (or descending) order for list l is checked by the function is_asorted(l) (or is_dsorted(l), respectively). The contract for the function snoc(l,x), which appends element x to the end of list l, states that if list l is sorted in descending order and leq_all(x,l) holds (that is, element x is less than or equal to every element of l), then also snoc(l,x) is sorted in descending order. In program Reverse we also need the function hd which, given a list of integers, returns a pair consisting of a boolean and an integer. If the given list is not empty and h is its head, then the returned pair is true, h , while it is false, 0 , if the list is empty, being 0 an arbitrary integer value (which is never used elsewhere in the program).  In order to prove the validity of a contract precond(x), postcond(x,f(x)) for a given function f, we need to prove that ∀x. precond(x) → postcond(x,f(x)). Now, if we submit to STAINLESS [14], which is a verifier for Scala programs, the above Reverse program with the initial directives: import stainless.proof._ import stainless.lang._ import stainless.collection._ we get that STAINLESS is not able to check the validity of the contract for rev, because it fails to establish (within the timeout of 100 s) the precondition for the function call 'snoc(rev(xs),x)' (occurring in the Cons case for rev), which is needed to use the postcondition of snoc and prove that rev(Cons(x, xs)) is sorted in descending order. Indeed, STAINLESS returns the following warning:

=> TIMEOUT case Cons(x, xs) => snoc(rev(xs),x)
In the next section we will see in action our technique for strengthening contracts in the case of the Reverse example. By using the strengthened contract for the function rev, STAINLESS is indeed able to construct, as desired, a proof of the validity of both contracts of that example, that is, the validity of the contracts for the functions rev and snoc.

Verifying Contracts via CHC Satisfiability
As already mentioned at the end of Section 1 our technique for strengthening the contracts is made out of four steps which we now perform in the case of the Reverse program shown in Figure 1.
Step (i). We translate the given Scala program and its contracts into the set ReverseCHCs of clauses shown in Figure 2. In this translation we maintain the call-by-value semantics of the Scala program in the sense that, if a function f applied to the input X evaluates to output Y, then the atom f(X,Y) occurs in the least model of the set ReverseCHCs.
Several techniques for translating imperative and functional programs have been defined in the literature [5,13]. Even if no specific tool is available, we may assume that, by applying one of those techniques we get a translation of Scala functions to CHC predicates that guarantees that the set ReverseCHCs is satisfiable if and only if the contracts for the functions rev and snoc of the program Reverse are valid. In Figure 2, the contracts for the functions rev and snoc are encoded by the two constrained goals GR and GS, respectively. Here and in what follows, we call 'constrained goal' (or 'goal', for short) any clause whose head is false.
Note that when writing clauses, we often prefer writing the variable X, instead of the constraint X=true, and the negated variable~X, instead of the constraint X=false. In particular, in clause GR of Figure 2 we have written (BL &~BR), instead of the equivalent constraint (BL=true & BR=false). Now, in order to show the validity of the contracts for rev and snoc, we have to show that the set ReverseCHCs of clauses is satisfiable. Unfortunately, the CHC solvers Eldarica and SPACER are not capable to solve this satisfiability problem. This is basically due to the fact that those solvers lack any form of inductive reasoning on lists and, moreover, they do not use the information about the validity of the contract for snoc during the proof of satisfiability of the goal which encodes the contract for rev.
Then, we proceed according to Step (ii) of our technique, which consists in applying a transformation that removes all ADT terms from ReverseCHCs. Indeed, we apply Algorithm T cata [9], implemented in the VeriCaT tool, and we get the new set TransfReverseCHCs of clauses (see Figure 3), whose satisfibility implies the satisfiability of the set ReverseCHCs. In particular, starting from goal GR, by transformation we obtain clauses T1-T5, and starting goal GS, by transformation we obtain clauses T6-T8.
Let us make a minor remark about the numbering of the new predicates occurring in clauses T1-T5 obtained by clause transformations starting from goal GR. (A similar remark applies to clauses T6-T8 when starting from goal GS.) VeriCaT uses for the new predicates to be introduced, a progressive numbering starting from the name new1, that is, it uses new1, new2, and so on. Now only predicates new3 and new7 occur in clauses T1-T5 because of the following two reasons: (i) during transformation, some of the new predicates that are introduced, are generalizations of already introduced ones, and thus one can replace the less general predicates by the more general ones, and (ii) some atoms with new predicates  It is not really important that the programmer understands the meaning of the newly introduced predicates, as they are obtained in a fully automatic way by an algorithm whose soundness is guaranteed in all cases. It is only important to note that all variables in TransfReverseCHCs are of sort boolean or integer. Indeed, Algorithm T cata always terminates and generates a set of clauses without ADT variables in the case where, as in our set ReverseCHCs of clauses, the contracts are specified by means of catamorphisms [9], that is, total functions defined by a simple recursion schema on the ADT structure. (The notion of catamorphism used here is an adaptation to CHCs of the one popularized by Meijer et al. [21] in the area of functional programming.) The kind of catamorphisms we have used in our example are all instances of the list catamorphism schema h for CHCs depicted in Figure 4. The recursion of predicate h is on its second argument, which has sort list. We leave to the reader to check that, indeed, the predicates is_asorted, is_dsorted, hd, and leq_all (see Figure 2) that we have used for specifying the contracts of rev and snoc, are all list catamorphisms. In particular, leq_all is a list catamorphism according to the schema of Figure   In Figure 4, we assume that: (i) f is a catamorphism defined by an instance of the same schema of that figure, (ii) the second arguments of h and f are of sort list, while all other arguments are of basic sort (either boolean or integer), and (iii) the predicate c defines a total function from its first four arguments to its last one.
As already mentioned, we have that if clauses T1-T5 are satisfiable then the contract for rev is valid and, likewise, if clauses T6-T8 are satisfiable then the contract for snoc is valid.
Having derived the set TransfReverseCHCs of clauses without ADT variables, we are ready to perform Step (iii) of our technique. Thus, we invoke a CHC solver (in our case SPACER) which, hopefully, is capable to prove the satisfiablity of TransfReverseCHCs, because in this set of clauses there are variables of basic sort only. Indeed, SPACER given clauses T1-T8, returns the answer 'sat' stating that TransfReverseCHCs is satisfiable. At this point, having proved the satifiability of TransfReverseCHCs, we have proved the validity of the contracts for rev and snoc. Now we know that the contracts for rev and snoc are valid, even if the contract for rev is not provable by STAINLESS. However, it is desirable to perform a further step (it is Step (iv) of our technique that we will describe in the next section) and derive strengthened contracts for rev and snoc whose validity can be automatically shown by STAINLESS, without appealing to an external verification system based on the first three steps of our technique. The need for those strengthened contracts comes from the software engineering requirement of having a single framework (Scala, in our case) where one specifies programs and contracts, and also proves contract validity (using STAINLESS, in our case). In the next section we will show how to comply with this requirement.
Note also that, with respect to the given contracts, the strengthened contracts provide a more detailed documentation of the program at hand, and they allow the programmer to better understand the correctness of the program, as the transformation-based proofs of the contracts are often hard to follow.

Strengthening Program Contracts using CHC Models
Now we show how to derive strengthened contracts for rev and snoc so that the STAINLESS verifier can prove their validity. This derivation can be done by: (1) taking into account the definitions of the new predicates introduced by VeriCaT during the CHC transformation of Step (ii), and (2) constructing the models of those new predicates as an outcome of the satisfiability proof of the CHCs performed by SPACER at Step (iii).
As we have mentioned at the end of Section 2, since STAINLESS is unable to show the contract for rev, while it is able to show the contract for snoc, we proceed by explaining how to get strengthened contracts by considering only the models of clauses T1-T5 relative to the rev contract. Those clauses refer to the new predicates new3 and new7 which VeriCaT introduced during Step (ii) by the following definition clauses (modulo variable renaming): (Note that, in order to eliminate the ADT variables, in the above clauses D3 and D7, the arguments of their head atoms are the variables of basic sort occurring in their associated bodies.) At Step (iii) SPACER shows the satisfiability of clauses T1-T5 by constructing models for new3 and new7. The model for new3 (BR,N,B (model for new7) First, we consider the definition clause D3 and the model M3 for new3. From the left conjunct (~IsDef => (BR & B)) of the model we have that if the list l is empty, being IsDef=false (see the clauses for hd in Figure 2), then: (i) the reversed list res is empty, (ii) res is vacuously sorted in descending order, and (iii) leq_all(n,res) vacuously holds for all integers n. Hence, we get the following formula (using the Scala syntax), where the variable n has been universally quantified (indeed, it is neither an input nor an output variable of rev): forall((n: BigInt) => (!(hd(l)._1) ==> (is_dsorted(res) && leq_all(n,res)))) From the second conjunct (BL => (BR & ( (Hd>=N) => B))) of the model M3 for new3, we get the following formula (again the variable n has been universally quantified): (3.2) forall((n: BigInt) => (is_asorted(l) ==> (is_dsorted(res) && ((hd(l)._2 >= n) ==> leq_all(n,res))))) Now the conjunction of the given postconditon of the function rev, that is, is_dsorted(res) (see the definition of rev in Figure 1), and formulas (3.1) and (3.2) can be suitably simplified by taking into account the precondition of rev, that is, is_asorted(l). After that simplification, we eventually get the strengthened postcondition for rev shown in Figure 5.
... ensuring { res => is_dsorted(res) && forall((n: BigInt) => ((!(hd(l)._1) ==> leq_all(n,res)) && ((hd(l)._2 >= n) ==> leq_all(n,res)))) } Then, it remains to consider the definition clause D7 and the model M7 for new7. Now BE can be replaced by true, because BE occurs in the atom leq_all(X,L,BE) in the body of clause D7 and by the precondition of snoc (see Figure 1), we have that leq_all(x,l) holds. Moreover, in the two atoms snoc(L,X,Res) and leq_all(J1,Res,K1) occurring in the body of clause D7, the value of the variable Res is that of res of the Scala function snoc, and the value of the variable K1 is the result of the Scala function leq_all(j1,res). Hence, from the model for new7, we get the following formula to be used for strengthening the postcondition for snoc: forall((j1: BigInt) => ((x >= j1)) ==> leq_all(j1,res))) where the variable j1 has been universally quantified, because it is neither an input nor an output variable of snoc. Thus, the conjunction of the given postcondition of snoc, that is, is_dsorted(res) (see the definition of snoc in Figure 1), and formula (7), gives us the strengthened postcondition for snoc shown in Figure 6.
By using these new, strengthened postconditions of the contracts for rev and snoc, instead of the old postconditions, we have that STAINLESS is able to prove the correctness of both contracts, as desired.
Let us briefly discuss the soundness of our technique for strengthening contracts. We consider the class of contracts specified by catamorphisms considered in previous work [9], where the termination of the transformation algorithm T cata is guaranteed. Soundness of our technique will be shown by proving that, if a given contract is valid and a CHC solver is able to prove the satisfiability of the set of clauses obtained by T cata , then also the strengthened version of the contract, which is derived by using our technique, is valid.
For reasons of simplicity, let us assume that we want to show the validity of a contract for the function f : α → β , where α and β are ADTs. Since the contract is specified by catamorphisms, its validity can be expressed by a formula of the form: where p 1 and p 2 are (tuples of) catamorphisms and c(v 1 , v 2 ) is a constraint on integer and boolean variables. For instance, in our Reverse example, C is the formula ∀ l, res, b1, b2. (rev(l) = res ∧ is_asorted(l) = b1 ∧ is_dsorted(res) = b2 → (b1 → b2)) Let us assume that the contract is valid. Thus, if we consider: (i) the set P of CHCs that translates the program including the function f, and (ii) the following goal G that translates the contract (where, as in Figure 2, '~' denotes boolean negation): G: false :-~c(V1, V2), f(X, Y), p 1 (X, V1), p 2 (Y, V2). then the set P ∪ {G} of CHCs is satisfiable.
Algorithm T cata introduces a new definition of the form: D: newf(V1, W1, V2, W2) :-f(X, Y), p 1 (X, V1), q 1 (X, W1), p 2 (Y, V2), q 2 (Y, W2). by using the catamorphisms p 1 and p 2 in G and adding (zero or more) new catamorphisms such as q 1 and q 2 coming from the contracts for other functions occurring in the program at hand. Let P ′ ∪ {G ′ } be set of CHCs produced as output by algorithm T cata . Some of the CHCs in P ′ have newf as the head predicate and G ′ is the goal derived from goal G.
If P ′ ∪ {G ′ } is proved to be satisfiable by any CHC solver, then there exists a model of P By using also goal G, we get: which shows the validity of a strengthened contract for f. Indeed, since catamorphisms are total functions, the atoms p 1 (X, V1), q 1 (X, W1), p 2 (Y, V2), and q 2 (Y, W2) are satisfiable, for all values of X and Y, and the conclusion of SC is strengthened with respect to the conclusion of C. Notice that, however, even if the strengthened contract is valid, we have no guarantee that the verifier (e.g., STAINLESS) is able to prove it.
Finally, let us make a remark on the minimality of the strengthened contracts, related to the fact that the information provided by the models of the new predicates introduced by algorithm T cata during program transformation, can also be used, so to say, in a partial way. Let us explain this point by referring to our program Reverse. In this case, instead of the strengthened postcondition for rev that is derived from the conjunction of the given postcondition is_dsorted(res) and formulas (3.1) and (3.2), we could have used the postcondition shown in Figure 7, which is derived from the given postcondition and formula (3.2) only.
... ensuring { res => is_dsorted(res) && forall((n: BigInt) => (((hd(l)._2 >= n) ==> leq_all(n,res)))) } This postcondition is sufficiently strong to allow the STAINLESS verifier to prove the contracts for rev and snoc (actually, STAINLESS does take for that proof less time with respect to the time taken for the more complex postcondition of Figure 5). However, in general, the strengthened postconditions that do not take into account the whole information which is derivable from the model of new predicates, provide a less informative description of the behaviour of the program functions at hand. We leave for future work the issue of computing minimally strengthened postconditions.

Conclusions
A good software engineering practice requires us to associate a contract with every program function, that is, to write, for each program function, a precondition and a postcondition.
The current software technology provides, together with compilers (and interpreters), also program verifiers, so that given a program function and its contract, one can execute the function and also prove its partial or total correctness with respect to its contract. Due to undecidability results, there is no program verifier that is able to prove (or disprove) program correctness in all cases. However, often a verifier is not able to show correctness simply because the contracts have not been specified in an adequate manner.
We have addressed this problem and we have proposed a technique which is capable of improving the contracts, and in particular, it is capable of strengthening their postconditions, so that a given verifier is successful in proving the correctness of functions, while it is not successful when trying to prove their correctness using the original postconditons.
We have considered programs and contracts written in the functional fragment of Scala and we have considered the STAINLESS [14] verifier for Scala programs. Our technique is based on the translation of the program functions and their contracts for which STAINLESS is not successful, into a set of constrained Horn clauses (CHCs) [5,13]. Then, in the case where programs manipulate Algebraic Data Structures, those clauses are transformed by VeriCaT [9], so that their satisfiability can hopefully be proved by SPACER (or a different CHC solver) in the domain of integers and/or booleans. If satisfiability is proved and a model for those clauses is found (which is defined by constraints on integers and/or booleans), then via a final translation step, we derive from that model suitable strengthened postconditions for the contracts. These derived contracts are guaranteed to be valid and can hopefully be proved by the STAINLESS verifier. However, at the moment, we do not have any general result characterizing these successful cases.
The derivation of strengthened contracts is an important objective from a software engineering point of view, because strengthened contracts provide a uniform framework (the Scala framework, in our case) where to write programs and their contracts. In this uniform framework an automatic system, such as STAINLESS, can show that the given contracts are valid. This is an important feature, because contracts can be viewed both as a documentation of the programs and also as a specification of their behavior.
As mentioned above, the proof of satisfiability of the CHCs derived after translation from the given programs, is already a proof of the contracts, but that proof is not given in the same framework. Moreover, it should rely on the correctness of the translation from Scala programs to CHCs and also on the correctness of the transformation for ADT removal. In addition, the derivation of strengthened postconditions and their proof done by STAINLESS increase the reliability of the validity proofs of the contracts, in the sense that the satisfiability preserving transformation performed by VeriCaT and the model constructed by the CHC solver SPACER are shown to agree with the behaviour of the STAINLESS Scala verifier. This agreement of automatic tools is very important in practice, and in particular when we deal with large programs.
Currently, we are working towards the full mechanization of the two steps of our technique that are still performed manually, even though they are performed in a systematic way, namely: (i) the semantic preserving translation from Scala programs into constrained Horn clauses, and (ii) the construction of strengthened postconditons from the models of the satisfiable clauses provided by a CHC solver (such as SPACER or Eldarica).