contract-prover

This package contains a tool to verify and add contracts in FlatCurry programs by proving contracts with an SMT solver. If a proof is successful, no contract check will be performed at run time, otherwise a dynamic (strict) contract check will be added. The static verification of contracts has the advantage that the resulting program will run more efficiently compared to a program with dynamic contract checking only/

A detailed description of the ideas of this tool can be found in the LOPSTR 2017 paper.

The tool is invoked via

> curry-contracts <Curry module>

This analyzes the FlatCurry code of the module, attempts to prove the contracts in this module (unless option --add is set), and adds dynamic contract checking if a proof is not successful. Finally, the FlatCurry program is replaced by the transformed version (unless option --target=NONE is set). Hence, this tool might be integrated into the compilation chain of a Curry system. In addition to the transformation of the FlatCurry program, successful proofs will be stored in files so that they can be re-used by other tools. For instance, if the postcondition of an operation f defined in module M is verified, a file PROOF_M_f_SatisfiesPostCondition.smt is generated. This file contains the SMT script of this proof.

The directory examples contains various examples where the contract prover can eliminate all contracts at compile time.

Implementation

In contrast to the first contract prover described in LOPSTR 2017 paper, which tried to remove contracts added by the Curry preprocessor, this version tries to verify contracts before they are added to the Curry program and adds dynamic checks only for unverified contracts (see the auxiliary operations defined in include/ContractChecker.curry).

The strategy is as follows:

  1. For each postcondition f'post, try to verify it. If this is not successful, a dynamic check is added to f.

  2. For each function call (f args), where a preconditon f'pre exists, try to verify this precondition in the given context of the call. If it cannot be verified, transform the function call into

    checkPreCond (f args) (f'pre args) "f" (args)

See include/ContractChecker.curry for the definition of checkPreCond.


Notes:


Directories of the package: