Combining Static and Dynamic Contract Checking for Curry

TL;DR

This paper proposes a combined static and dynamic contract checking approach for the Curry language, reducing runtime overhead and increasing reliability by verifying contracts at compile time whenever possible.

Contribution

It introduces an automatic method to verify contracts at compile time in Curry, allowing omission of dynamic checks and enhancing program safety and efficiency.

Findings

Contracts can be verified at compile time, reducing runtime checks.

When all contracts are verified statically, runtime crashes due to violations are eliminated.

The approach improves program reliability and performance in Curry.

Abstract

Static type systems are usually not sufficient to express all requirements on function calls. Hence, contracts with pre- and postconditions can be used to express more complex constraints on operations. Contracts can be checked at run time to ensure that operations are only invoked with reasonable arguments and return intended results. Although such dynamic contract checking provides more reliable program execution, it requires execution time and could lead to program crashes that might be detected with more advanced methods at compile time. To improve this situation for declarative languages, we present an approach to combine static and dynamic contract checking for the functional logic language Curry. Based on a formal model of contract checking for functional logic programming, we propose an automatic method to verify contracts at compile time. If a contract is successfully verified, dynamic checking of it can be omitted. This method decreases execution time without degrading reliable program execution. In the best case, when all contracts are statically verified, it provides trust in the software since crashes due to contract violations cannot occur during program execution.