A Refinement Theory for Concurrent Object Oriented Languages

Abstract

A notion of refinement for concurrent object-oriented programs was originally presented in [3]. In this article we prove that the refinement relation associated to this notion is a congruence with respect to various standard programming language constructors, including parallel and sequential composition, conditionals, and non-deterministic internal choice. We also establish a weaker compositionality result for the atomic evaluation constructor, and illustrate how novel compositionality properties can be derived from the basic congruence property.