Concurrent Object-Oriented Programs: From Specification to Code

In this paper we put forward a concurrent object-oriented programming language in which concurrency is tightly integrated with objects. Concurrency is expressed by extending classes with actions and allowing methods to be guarded. Concurrency in an object may be hidden to the outside, thus allowing concurrency to be introduced in subclasses of a class hierarchy. A disciplined form of intra-object concurrency is supported. The language is formally defined by translation to action systems. Inheritance and subtyping is also considered. A theory of class refinement is presented, allowing concurrent programs to be developed from sequential specifications. Our goal is to have direct rules for verification and refinement on one hand and a practical implementation on the other hand. We briefly sketch our implementation. While the implementation relies on threads, the management of threads is hidden to the programmer.