×

zbMATH — the first resource for mathematics

Observability, connectivity, and replay in a sequential calculus of classes. (English) Zbl 1143.68359
de Boer, Frank S. (ed.) et al., Formal methods for components and objects. Third international symposium, FMCO 2004, Leiden, The Netherlands, November 2–5, 2004. Revised lectures. Berlin: Springer (ISBN 3-540-29131-8/pbk). Lecture Notes in Computer Science 3657, 296-316 (2005).
Summary: 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.
For the entire collection see [Zbl 1084.68008].

MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
PDF BibTeX Cite
Full Text: DOI