Higher-Order Contracts for Actor Based Languages

Christophe Scholliers, Wolfgang De Meuter, Eric Tanter

Onderzoeksoutput: Editorial


The use of assertion based contracts is a widely deployed software
engineering practice. Contracts help programmers to document interfaces,
detect interface violations and identify the responsible
party in case of a violation. The use of contracts in a communicating
event loop system is currently limited to the validation of values
which are passed by copy. Guaranteeing non-interference for assertions
defined over remote objects is significantly more complex
than verifying the same assertions over a local object which can be
accessed synchronously. Contract verification algorithms that make
use of blocking can introduce deadlocks or alter the order in which
messages are processed. In this paper we propose a novel asynchronous
contract system where the validation of assertions over remote
objects are postponed until a message is sent to the contracted
remote object. By postponing the verification non-interference of
the contract with respect to deadlocks and message ordering semantics
can be ensured.We describe an expressive model to specify and
verify asynchronous higher-order contracts over remote objects, including
proper blame assignment.
Originele taal-2English
Aantal pagina's9
TijdschriftUnknown Journal
StatusPublished - 1 dec 2011

Citeer dit