F. Honsell, M. Lenisa, and R. Redamalla
Coalgebraic semantics and observational equivalences of an imperative
class-based oo language
Technical Report 02/2003, Dipartimento di Matematica e Informatica,
Università di Udine, Italy, 2003
We study two observational equivalences of Fickle
programs. Fickle is a class-based object oriented imperative language,
which extends Java with object re-classification. The first is
a contextual equivalence of expressions with respect to a given
program. We provide an adequate coalgebraic semantics
for it,
which is compositional w.r.t. the operators of the language.
The second observational equivalence is defined on programs
implementing the same specification, given as an abstract
class. We introduce a coalgebraic description of classes which gives a sound
coinduction principle for this latter equivalence.
To this end we need to extend the original coalgebraic approach
of H.Reichel and B.Jacobs to deal with binary
methods, i.e. methods which take more than one instance of the
hosting class as argument. This coalgebraic description induces in
particular a
coinductive observational
equivalence on
objects of a program, where objects (states of a class)
are taken to be equal when the action of methods on them yield the
same observations and equivalent next states.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43