Connexion

English version

PPS UMR 7126 – Laboratoire
Preuves, Programmes et Systèmes

Accueil · Présentation · Membres · Publications · Séminaire · Groupes de travail · Projets · πr²

Luca Padovani

The Chemical Approach to Typestate-Oriented Programming

In an object-oriented program, the interface of an object describes the whole set of methods supported by the object throughout its entire lifetime. However, the usage of the object is more precisely explained in terms of its protocol, describing the sequences of method calls that are legal, possibly depending on the object's internal state. Typestate-oriented programming (TSOP for short) is a programming discipline that encourages programmers to develop objects around their protocol and enables the compiler to verify that programs comply with the protocols of the objects they use. In this work we extend TSOP to concurrent objects - objects that are accessed and possibly modified by several concurrent processes. We show that the Objective Join Calculus is an extremely natural model for concurrent TSOP and we detail the first behavioral type system for the Objective Join Calculus, which allows us to describe object interfaces, to verify protocol compliance, and to control object sharing.