论文标题
通过约束的喇叭条款验证加强合同
Contract Strengthening through Constrained Horn Clause Verification
论文作者
论文摘要
程序的功能属性通常是通过为其每个功能提供合同来指定的。功能的合同由一对公式组成，称为前提条件和后条件，该公式分别应在执行该函数之前和之后保持。可能是程序员提供的合同不足以允许验证系统证明程序正确性，也就是说，表明对于每个函数，如果先前的条件持有并且执行函数终止，则后条件结构。我们通过提供一种可以加强功能后条件的技术来解决此问题，从而提高验证者显示程序正确性的能力。我们的技术包括四个步骤。首先，给定程序的翻译可能会操纵代数数据结构（ADT）及其合同为一组受约束的Horn条款（CHC），其可满足性意味着给定合同的有效性。然后，通过Vericat工具执行的CHC转换的派生，这些新的CHC集仅操纵基本类型（例如布尔值或整数），并且其可满足性意味着原始条款集的满意度。然后，使用CHC求解器垫片进行基本种类的新型CHC的模型（如果有的话）的构建。最后，将该模型转换为适当加强给定合同后条件的公式。我们将通过一个示例介绍我们的技术，该示例包括用于逆转列表的Scala程序。请注意，不锈钢验证者在考虑给定合同时无法证明该计划的正确性，而在考虑通过应用我们的技术构建的加强后条件时，它成功了。
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.
