zbMATH — the first resource for mathematics

Bisimulations for untyped imperative objects. (English) Zbl 1178.68154
Sestoft, Peter (ed.), Programming languages and systems. 15th European symposium on programming, ESOP 2006, held as part of the joint European conferences on theory and practice of software, ETAPS 2006, Vienna, Austria, March 27–28, 2006. Proceedings. Berlin: Springer (ISBN 3-540-33095-X/pbk). Lecture Notes in Computer Science 3924, 146-161 (2006).
Summary: We present a sound and complete method for reasoning about contextual equivalence in the untyped, imperative object calculus of M. Abadi and L. Cardelli [A theory of objects. New York, NY: Springer-Verlag (1996; Zbl 0876.68014)]. Our method is based on bisimulations, following the work of Sumii and Pierce (2004, 2005) and our own [V. Koutavas and M. Wand, “Smaller bisimulations for reasoning about higher-order imperative programs”, in: Proc 33rd annual ACM symposium on principles of programming languages (2006)]. Using our method we were able to prove equivalence in more complex examples than the ones of Gordon, Hankin and Lassen (1997) and Gordon and Rees (1998). We can also write bisimulations in closed form in cases where similar bisimulation methods require an inductive specification. To derive our bisimulations we follow the same technique as we did in our previous work [loc. cit.], thus indicating the extensibility of this method.
For the entire collection see [Zbl 1103.68010].

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Full Text: DOI