Coalgebraic Theory And Its Applications On Formal Methods For Object-Oriented System

The object-oriented technique, whose models describe the real world activities in a natural way, has been widely used in the design and construction of software systems. The objects in the models are the direct simulation of the entities in the real world and the virtual world. Developing software with object-oriented technique, which can make the software development processe more natural and, thus, promotes software productivity, can minimize the semantic gap between problem and solution. The kernel component of the object-oriented system is class, which represents the essencial, important and observable behavior of the objects. Therefore, to evaluate the coding implemention of class, it's essential how the completeness degree of an objective concept expressed by a class is judged.In the marking task of programming problems, computer-aided marking system mainly focuses on the validity of the program result and the completeness of the function. It still emphasizes the structured design thought, but does not support the object-oriented patterns which have been used widely. So the system can not evaluate the students' ability to analyze and solve problems through object-oriented approach. The main concern of this paper is theorical and practical researching on the implementation of automatic semantic analysis in object-oriented programming field. The formal method is utilized to analyze and verify the similarity between the coding implemention and objective concept in semantic level.Coalgebra, which is the formal dual of algebra, is introduced as mathematical model of class implementation. Comparing with the study of the constructive element of data types in traditional algebraic methods, the observable behavior of system is investigated in coalgebraic methods, which have distinct advantages in mathematic study of state-based systems.In this paper, the theories of coalgebra are introduced, including the basic concepts, categorical foundations, logical foundations and its applications on the formal semantic analysis for object-oriented system. The formal verificationtechnology and coalgenraic semantic specification is combined to create a model for measuring the similarity degree between class and concept. In this model, coalgebraic class specification language CCSL is used to represent objective concepts and translated into the high-order logic. Finally the theory prover PVS is utilized to verify the validity of the assertion in the implemention model.