A formal framework with late binding

Abstract

We define a specification formalism (formally, an institution) which provides a notion of dynamic type (the type which is associated to a termb y 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 dynamicallytyped languages and a basis for adding to thema 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.