Reasoning about concurrent objects

Embedded specifications in object-oriented (OO) languages such as Eiffel and Sather are based on a rigorous approach towards validation, compatibility and reusability of sequential programs. The underlying method of "design-by-contract" is based on Hoare logic for which concurrency extensions exist. However concurrent OO languages are still in their infancy. They have inherently imperative facets, such as object identity, sharing, and synchronisation, which cannot be ignored in the semantics. Any marriage of objects and concurrency requires a trade-off in a space of intertwined qualities. The paper summarises our work on a type system, calculus and an operational model for concurrent objects in a minimal extension of the Eiffel and Sather languages (cSather). We omit concurrency control constructs and instead use assertions as synchronisation constraints for asynchronous functions. We show that this provides a framework in which subtyping and concurrency can coexist.