Contract Monitoring and Call-by-name Evaluation (extended abstract)

Markus Degen, Peter Thiemann, and Stefan Wehr

In 20th Nordic Workshop on Programming Theory. Tallinn, Estonia. November 2008.

Abstract

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 an established theoretical basis. For languages with call-by-name evaluation, several styles of contract monitoring are possible. In this article, we study two such styles: 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.

Bibtex

@INPROCEEDINGS{DegenThiemannWehr2008,
  author = {Markus Degen and Peter Thiemann and Stefan Wehr},
  title = {Contract Monitoring and Call-by-name Evaluation (extended abstract)},
  booktitle = {20th Nordic Workshop on Programming Theory},
  month = {November},
  year = 2008,
  address = {Tallinn, Estonia}
}

Resources

• Preprint: .pdf