Published in Volume XXII, Issue 1, 2012, pages 5-60, doi: 10.7561/SACS.2012.1.5

Authors: M. Bartoletti, E. Tuosto, R. Zunino


We present CO2, a parametric calculus for contract-based computing in distributed systems. By abstracting from the actual contract language, our calculus generalises both the contracts-as-processes and contracts-as-formulae paradigms. The calculus features primitives for advertising contracts, for reaching agreements, and for querying the fulfilment of contracts. Coordination among participants happens via multi-party sessions, which are created once agreements are reached. We present two instances of our calculus, by modelling contracts as processes in a variant of CCS, and as formulae in a logic. We formally relate the two paradigms, through an encoding from contracts-as-formulae to contracts-as-processes which ensures that the promises deducible in the logical system are exactly those reachable by its encoding as a process. Finally, we present a coarse-grained taxonomy of possible misbehaviours in contract-oriented systems, and we illustrate them with the help of a variety of examples.

Full Text (PDF)


[1] Alexander Artikis, Marek J. Sergot, and Jeremy V. Pitt. Specifying norm-governed computational societies. ACM Trans. Comput. Log., 10(1), 2009.

[2] Massimo Bartoletti, Emilio Tuosto, and Roberto Zunino. Contracts in distributed systems. In ICE, volume 59 of EPTCS, pages 130-147, 2011.

[3] Massimo Bartoletti and Roberto Zunino. A logic for contracts. Technical Report DISI-09-034, DISI – Universit a di Trento, 2009.

[4] Massimo Bartoletti and Roberto Zunino. A calculus of contracting processes. In LICS, pages 332-341. IEEE Computer Society, 2010.

[5] Massimo Bartoletti and Roberto Zunino. Primitives for contract-based synchronization. In ICE, volume 38 of EPTCS, pages 67-82, 2010.

[6] Laura Bocchi, Kohei Honda, Emilio Tuosto, and Nobuko Yoshida. A theory of design-by-contract for distributed multiparty interactions. In CONCUR, volume 6269 of Lecture Notes in Computer Science, pages 162-176. Springer, 2010.

[7] Mario Bravetti and Gianluigi Zavattaro. Towards a unifying theory for choreography conformance and contract compliance. In Software Composition, volume 4829 of Lecture Notes in Computer Science, pages 34-50. Springer, 2007.

[8] Maria Grazia Buscemi and Hern an C. Melgratti. Transactional service level agreement. In TGC, volume 4912 of Lecture Notes in Computer Science, pages 124-139. Springer, 2007.

[9] Maria Grazia Buscemi and Ugo Montanari. CC-Pi: A constraint-based language for specifying service level agreements. In ESOP, volume 4421 of Lecture Notes in Computer Science, pages 18-32. Springer, 2007.

[10] Felice Cardone. The geometry and algebra of commitment. In Ludics, dialogue and interaction, pages 147-160. Springer, 2011.

[11] Samuele Carpineti, Giuseppe Castagna, Cosimo Laneve, and Luca Padovani. A formal account of contracts for web services. In WS-FM, volume 4184 of Lecture Notes in Computer Science, pages 148-162. Springer, 2006.

[12] Samuele Carpineti and Cosimo Laneve. A basic contract language for web services. In ESOP, volume 3924 of Lecture Notes in Computer Science, pages 197-213. Springer, 2006.

[13] Giuseppe Castagna, Nils Gesbert, and Luca Padovani. A theory of contracts for web services. ACM Transactions on Programming Languages and Systems, 31(5), 2009.

[14] Giuseppe Castagna and Luca Padovani. Contracts for mobile processes. In Proc. CONCUR, volume 5710 of Lecture Notes in Computer Science, pages 211-228. Springer, 2009.

[15] Mario Coppo and Mariangiola Dezani-Ciancaglini. Structured communications with concurrent constraints. In TGC, volume 5474 of Lecture Notes in Computer Science, pages 104-125. Springer, 2008.

[16] Mads Dam. On the Decidability of Process Equivalences for the pi-calculus. Theoretical Computer Science, 183(2):215-228, 1997.

[17] E. Allen Emerson. Temporal and modal logic. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pages 995-1072. North-Holland Pub. Co./MIT Press, 1990.

[18] Gian Luigi Ferrari and Alberto Lluch-Lafuente. A logic for graphs with QoS. Electr. Notes Theor. Comput. Sci., 142:143-160, 2006.

[19] Deepak Garg and Martin Abadi. A modal deconstruction of access control logics. In FoSSaCS, volume 4962 of Lecture Notes in Computer Science, pages 216-230. Springer, 2008.

[20] Thomas Hobbes. Leviathan or The Matter, Forme and Power of a Common Wealth Ecclesiasticall and Civil. 1651. Chapter XIV | Of the first and second natural laws, and of contracts.

[21] Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. Language primitives and type disciplines for structured communication-based programming. In ESOP, volume 1381, 1998.

[22] Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronoussession types. In POPL, pages 273-284. ACM, 2008.

[23] Ashley T. McNeile. Protocol contracts with application to choreographed multiparty collaborations. Service Oriented Computing and Applications, 4(2):109-136, 2010.

[24] Robin Milner. Communication and concurrency. Prentice-Hall, Inc., 1989.

[25] Cristian Prisacariu and Gerardo Schneider. A formal language for electronic contracts. In FMOODS, volume 4468 of Lecture Notes in Computer Science, pages 174-189. Springer, 2007.

[26] Cristian Prisacariu and Gerardo Schneider. A dynamic deontic logic for complex contracts. The Journal of Logic and Algebraic Programming (JLAP), 81(4):458-490, 2012.

[27] Vijay Saraswat, Prakash Panangaden, and Martin Rinard. Semantic foundations of concurrent constraint programming. In POPL, pages 333-352, 1991.

[28] Anne Troelstra and Dirk van Dalen. Constructivism in Mathematics, vol. 1. North-Holland, 1988.


  title={Contract-Oriented Computing in CO2},
  author={M. Bartoletti and E. Tuosto and R. Zunino},
  journal={Scientific Annals of Computer Science},
  organization={``A.I. Cuza'' University, Iasi, Romania},
  publisher={``A.I. Cuza'' University Press}