Axiomatic Semantics Of Class And Polymorphism For Java

In this paper, we mainly discuss the axiomatic semantics of class and polymorphism for Java, including the correlative component. The content of the paper covers:(1) Give the axiomatic semantics of class, including the axiomatic semantics of declaration of class, static method of class, constructor and data members.(2) Give the axiomatic semantics of object, including the axiomatic semantics of the new instance creation expression and the instance method invocation.(3) Array is an object, so we give the axiomatic semantics of array, including the axiomatic semantics of array creation expression and array access expression.(4) The inherence of class and polymorphism is a mechanism rather than a language component, so it is described in the different ways from the above three kinds.With the development of programming design, people pay attention to the correctness, reliability and maintainability and so on. Many formal methods of programming specification and formal correctness proof appear, which take an important role in the development of the methodology for programming design. While object-oriented principals are widely used and gain increasing importance in today's software development, the formal correctness proof is still a hard problem. The most widely used method in the formal correctness proof is the Hoare method. It uses inductive formulas characterizing input/output relationships of programs or program segments. Object invariant describes the relationship of the object-oriented data structure, it always holds true after the object creation and on the entrance and exit of the method invocation. Object invariant is important in the object-oriented program proof. Using object invariants, class invariants, the state of static data members and instance data members, and Hoare axiom system, we definitely give the axiomatic semantics of class.Polymorphism is an import character and hard to be understood in the object-oriented programming design, so it's easy to make a mistake when using it. When describe its axiomatic semantics, there are a lot of tasks which should be resolved because we use static attributes to describe dynamic attributes. This paper introduces new predication and function to select the precondition and postcondition, we describe the axiomatic semantics of polymorphism.Using the axiomatic semantics which are given, we can compile and interprete the production of Java program; they also can check the correctness of the programs.