Lazy and Enforceable Assertions for Functional Logic Programs

Assertions or contracts are an important technique to improve the quality of software. Thus, assertions are also desirable for functional logic programming. Unfortunately, there is no established meaning of assertions in languages with a demand-driven evaluation strategy. Strict assertions are immediately checked but may influence the behavior of programs. Lazy assertions do not modify the behavior but may not be faithful since some assertions might not be checked at all. In order to avoid the disadvantages of strict and lazy assertions, the authors propose enforceable assertions that are delayed as lazy assertions but can be explicitly enforced at some point where faith is required, e.g., at the end of the program execution or before irrevocable I/O actions.