Dipartimento di Informatica e Scienze dell'Informazione
A Formal Framework with Late Binding
D. Ancona ,
M. Cerioli and
E. Zucca .
In Jean-Pierre Finance, editor, Proceedings of FASE'99,
number 1577 in Lecture Notes in Computer Science, pages 30--44, Berlin, 1999.
We define a specification formalism (formally, an institution) which provides
a notion of dynamic type (the type which is associated to a term by a
particular evaluation) and late binding (the fact that the function version
to be invoked in a function application depends on the dynamic type of one or
more arguments). Hence, it constitutes a natural formal framework for modeling
object-oriented and other dynamically-typed languages and a basis for
adding to them a specification level. In this respect, the main novelty is the
capability of writing axioms related to a given type which are not required to
hold for subtypes, hence can be "overridden" in further refinements, thus
lifting at the specification level the possibility of reusing code which is
by the object-oriented approach.
The compressed postscript version of this paper is available through anonymous ftp
at ftp.disi.unige.it, in