Technical Report No. 243 - Abstract

Markus Degen, Peter Thiemann, Stefan Wehr
Contract Monitoring and Call-by-name Evaluation

Contracts are a proven tool in software development. They provide specifications for operations that may be statically verified or dynamically validated by contract monitoring. Contract monitoring for strict languages has a by now established theoretical basis. This article investigates the properties of contract monitoring for languages with call-by-name evaluation. We study two different styles of contract monitoring: eager monitoring enforces a contract when it is demanded, possibly evaluating expressions not touched by the user code, whereas delayed monitoring only proceeds as far as the user code itself can observe. In each case, an effect system ensures that contract monitoring does not change the meaning of a program and guarantees that contract monitoring is idempotent. Our formalization brings forward semantic reasons that favor delayed monitoring for a call-by-name language and comes with a Haskell implementation.