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.

The problem of correctness of a class C w.r.t. a specification S is discussed. A formal counterpart of the problem is the question well known in metamathematics, whether an algebraic structure is a model of a given theory. Now, this metamathematical problem has to be adapted to the context of software engineering. As a theory we consider the (algorithmic) specification S. The algebraic structure A _C induced by the class C is our candidate for a model of S. Remark, that this problem differs from the correctness' problem of an algorithm w.r.t. a pre- and a post-conditions. In the paper we consider the specification ATPQ of priority queues and the class PQS, and we verify the correctness of this class with respect to the specification ATPQ. Programmers and software companies prefer to test software instead of proving it. Surely, proving is more difficult, testing is easier. In this article we combine these two approaches. Hence, the following actions appear in our method of verification: experiment, observe, formulate hypotheses, prove. It is our hope that this method is of general use and adapts well to many practical cases of verification of object-oriented software.

We consider first-order specifications together with the restriction to accept only programmable algebras as models. We provide a criterion which links this approach with the "generation principle": all programmable models of any specification SP that meets this criterion are reachable. We also show an example of a specification which does not satisfy the criterion and admits a programmable yet nonreachable model. Moreover, a general method of showing the existence of programmable but nonreachable models for a class of first-order specifications is given.

It is commonly believed that a programmable model satisfying the axioms of a given algebraic specification guarantees good properties and is a correct implementation of the specification. This convinction might be related to the Tennenbaum's property