Higher-Order Contracts for Actor Based Languages

Research output: Contribution to journalEditorial

Abstract

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.
Original languageEnglish
Number of pages9
JournalUnknown Journal
Publication statusPublished - 1 Dec 2011

Keywords

  • Contracts
  • Assertions

Cite this