Furio Honsell, Marina Lenisa, and Rekha Redamalla
Coalgebraic semantics and observational equivalences of an imperative
class-based oo-language
In Furio Honsell, Marina Lenisa, and Marino Miculan, editors,
Proc. COMETA'03, ENTCS, pages 146-162, Udine, Italy, December 2003
Elsevier/Forum
Fickle is a class-based object oriented imperative
language, which extends Java with object
re-classification. In this paper, we
introduce a natural observational equivalence
over Fickle programs. This is a
contextual equivalence over main
methods with respect to a given sequence of class
definitions, i.e. a program. In order to study it,
we utilize the formal computational model for
OO-programming based on coalgebras, which has
recently emerged, whereby objects are taken to be
equal when the actions of methods on them yield the
same observations and equivalent next
states. However, in order to deal with
imperative features, we need to extend the original
approach of H.Reichel and B.Jacobs in various
ways. In particular, we introduce a
coalgebraic description of objects (states of
a class), which induces a coinductive
behavioural equivalence on programs. For
simplicity, we focus on Fickle objects whose
methods do not take more than one object parameter
as argument. Completeness results as well as
problematic issues arising from binary
methods are also discussed.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43