An event-based model for contracts

Massimo Bartoletti
(Universita' degli Studi di Cagliari)
Tiziana Cimoli
(Universita' degli Studi di Cagliari)
G. Michele Pinna
(Universita' degli Studi di Cagliari)
Roberto Zunino
(DISI-Universita' degli Studi di Trento and COSBI, Italy)

We introduce a basic model for contracts. Our model extends event structures with a new relation, which faithfully captures the circular dependencies among contract clauses. We establish whether an agreement exists which respects all the contracts at hand (i.e. all the dependencies can be resolved), and we detect the obligations of each participant. The main technical contribution is a correspondence between our model and a fragment of the contract logic PCL. More precisely, we show that the reachable events are exactly those which correspond to provable atoms in the logic. Despite of this strong correspondence, our model improves previous work on PCL by exhibiting a finer-grained notion of culpability, which takes into account the legitimate orderings of events.

In Simon Gay and Paul Kelly: Proceedings Fifth Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software (PLACES 2012), Tallinn, Estonia, 31 March 2012, Electronic Proceedings in Theoretical Computer Science 109, pp. 13–20.
Published: 23rd February 2013.

ArXived at: https://dx.doi.org/10.4204/EPTCS.109.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org