DISI 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. Springer Verlag.
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 offered by the object-oriented approach.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /pub/person/AnconaD/LateBinding.ps.gz (79522 Kb)