An Open System Operational Semantics for an Object-Oriented and Component-Based Language

Object orientation and component-based development have both proven useful for the elaboration of open distributed systems. These paradigms are offered by the Creol language. Creol objects are concurrent, each with its own virtual processor and internal process control, and communicate using asynchronous (non-blocking) method calls. This provides the efficiency of message passing systems, while keeping the structuring benefits of methods and object-oriented programming. Conditional processor release points provide a high-level synchronization mechanism based on passive waiting that allows us to combine active and reactive behavior. A Creol component can be a single (concurrent) object or a collection of objects, together with a number of interfaces, and cointerfaces, defining the provided and required interaction and semantic behavior. Creol's semantics is defined formally using operational semantics and Hoare logic. An operational semantics lets us simulate an entire system, where all components are known in advance; in contrast, Hoare logic, together with class invariants and communication histories, lets us reason locally about a method body, without needing access to the implementations of the other classes. To bridge the gap between these two semantics, we introduce a history-based operational semantics for open systems. This new semantics can be used as an intermediate step for proving that Creol's Hoare logic is sound and complete with respect to the language's operational semantics. The approach can easily be adapted to other component-based languages where communication is done by message passing or by method interaction.