We have formally defined the dynamic semantics of the Eiffel language using Natural Semantics, and more precisely object-oriented features such as message passing, multiple inheritance, polymorphism, redefinition and renaming, and dynamic binding [8].
Using the Centaur system, we have produced a definition of the dynamic semantic aspects of Eiffel which provides us with an interpreter for Eiffel programs and permits to head towards formal verification of, and transformations on, Eiffel programs.
The dynamic semantic specification assumes that the static semantics of the Eiffel system is correct, and is written using the abstract syntax of the Eiffel language. An Eiffel system performs computations on objects. An object (instance of a class), has an initial part which represents its type; usually called dynamic type in contrast to the static type of the program entities. During the execution of an Eiffel system, a list of such objects is created, used and modified.
Many dynamic semantic specifications define environments that reflect the block structure of languages. During interpretation, environments (symbol tables), for each block, are built and used to handle visibility rules, hiding, and so on. When specifying the semantics of an object-oriented language, the equivalent would be to compute, for every class, the inherited features, the attribute list, and so on. We did not use this technique because we consider it to be too operational since it requires to build some intermediate data structures.
When specifying one aspect of the program semantics, we typically require information about other parts of the program. This is obtained directly from the appropriate part of the abstract syntax tree of the program thanks to our axiomatic specifications. We believe this method to be more descriptive and so more abstract. However, since our semantic definition is executable, this choice does not favor efficiency, but the main concern here is to define a compact and readable semantic definition. In our model, the dynamic binding between a routine name and its actual body is computed on the fly, according to the current object, polymorphism and inheritance.
The use of the Natural Semantics approach appeared to be a good choice for the definition of the dynamic semantics of an object-oriented language. It is quite compact, the current Eiffel definition is nearly 200 inference rules and axioms in approximately 1000 lines. The benefits from interpreting the semantics with the Centaur system were also very significant. A graphical environment makes it possible to develop the semantics using step by step refinements, to see the current rule applied for the proof with all the variable values. Moreover, the resulting interpreter can be animated, i.e. highlighting the feature call currently executed, highlighting the object the feature is currently applied on, and showing the changes occurring on the list of objects.