Observability, connectivity, and replay in a sequential calculus of classes

Abstract

Object calculi have been investigated as semantical foundation for object-oriented languages. Often, they are object-based, whereas the mainstream of object-oriented languages is class-based. Considering classes as part of a component makes instantiation a possible interaction between component and environment. As a consequence, one needs to take connectivity information into account. We formulate an operational semantics that incorporates the connectivity information into the scoping mechanism of the calculus. Furthermore, we formalize a notion of equivalence on traces which captures the uncertainty of observation cause by the fact that the observer may fall into separate groups of objects. We use a corresponding trace semantics for full abstraction wrt. a simple notion of observability. This requires to capture the notion of determinism for traces where classes may be instantiated into more than one instance during a run and showing thus twice an equivalent behavior (doing a "replay"), a problem absent in an object-based setting. © Springer-Verlag Berlin Heidelberg 2005.