Computational contracts

Software contracts have proven to play an important role for the development of robust software. Contract systems are widely adopted in statically typed languages and are currently finding their entrance in dynamically-typed programming languages. Most research on higher-order contracts has adopted a black-box approach where only input and output are checked. These systems cannot check many interesting concerns about the behaviour of a function. Examples include prohibiting or ensuring that certain functions are called, checking access permissions, time or memory constraints, interaction protocols, etc. To address this need for behavioural runtime validation, while preserving support for higher-order programming, we introduce the notion of computational contracts. Computational contracts is a contract model with blame assignment in a higher-order setting that provides a systematic way to specify temporal contracts over objects and functions and their possibly higher-order arguments. We show various applications of computational contracts, and explain how to assign blame in case of a violation. Computational contracts have been integrated in both Scheme and AmbientTalk, a dynamically-typed object-oriented language built upon the principles of prototype-based programming.