Computational Contracts

Pre/post contracts for higher-order functions, as proposed by Findler and Felleisen and provided in Racket, allow run-time verification and blame assignment of higher-order functions. However these contracts treat contracted functions as black boxes, allowing verification of only input and output. It turns out that many interesting concerns about the behaviour of a function require going beyond that black-box approach, in order to control the actual computation that follows from a function. Examples are prohibiting or verifying that certain functions are called, checking access permissions, time or memory constraints, interaction protocols, etc.

Provided by: Vrije Universiteit Brussel Topic: Software Date Added: Sep 2011 Format: PDF

Find By Topic