Execution semantics for rCOS

rCOS, the abbreviation of Refinement Calculus for Object Systems, is designed to present mathematical characterization of essential object-oriented concepts for an object-based language with a rich variety of features including subtypes, inheritance, type casting, dynamic binding and polymorphism. This paper represents an operational semantics for the rCOS language based on labeled transition systems. The result semantics shows the process of how the effects of an rCOS program are produced. It can be a secure guide for the implementation of the rCOS language, which is being carried out by our group. For the purpose of extending verifiability and functionality, a set of auxiliary language features is introduced to the rCOS language. Concurrent execution structure is designed to specify multi-threaded programs. Also the simulation is introduced to specify the observable behaviors of objects, and it can be regarded as the refinement relation defined in denotational domain to some extent.