Affiliations: Institut für Informatik, Christian-Albrechts-Universität zu Kiel, Christian-Albrechts-Platz 4, D-24098 Kiel, Germany. [email protected] | Faculty of Mathematics and Informatics, University Cardinal Stefan Wyszyński, Wóycickiego 1-3, 01-938 Warszawa, Poland. [email protected]
Note: [] Address for correspondence: Christian-Albrechts-Universität zu Kiel, Christian-Albrechts-Platz 4, D-24098 Kiel, Germany
Abstract: In [14] an axiomatic approach towards the semantics of FJI, Featherweight Java with Inner classes, essentially a subset of the Java-programming language, is presented. In this way the authors contribute to an ambitious project: to give an axiomatic definition of the semantics of programming language Java. At a first glance the approach of reducing Java's semantics to that of FJI seems promising. We are going to show that several questions have been left unanswered. It turns out that the theory how to elaborate or bind types and thus to determine direct superclasses as proposed in [14] has different models. Therefore the suggestion that the formal system of [14] defines the (exactly one) semantics of Java is not justified. We present our contribution to the project showing that it must be attacked from another starting point. Quite frequently one encounters a set of inference rules and a claim that a semantics is defined by the rules. Such a claim should be proved. One should present arguments: 1° that the system has a model and hence it is a consistent system, and 2° that all models are isomorphic. Sometimes such a proposed system contains a rule with a premise which reads: there is no proof of something. One should notice that this is a metatheoretic property. It seems strange to accept a metatheorem as a premise, especially if such a system does not offer any other inference rules which would enable a proof of the premise. We are going to study the system in [14]. We shall show that it has many non-isomorphic models. We present a repair of Igarashi's and Pierce's calculus such that their ideas are preserved as close as possible.
Keywords: object oriented programming, semantics, inheritance, inner classes, direct superclass, static semantics analysis, static binding, derivation calculus, model, minimal resp. least model
