A Refinement Theory for Concurrent Object Oriented Languages - Borba, Paulo (Anais do Simpósio Brasileiro de Engenharia de Software (SBES), 1996)
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.