关键词: 面向对象方法，形式语义，共代数方法，强Monads

Abstract: According to the problems of relative weak mathematical theory foundations of object oriented methods, the coalgebraic methods were used to analyze the formal semantics of object oriented methods from the perspectives of category theory and observation. Firstly,we presented the coalgebraic descriptions of classes and objects,among which abstract class was defined as a class specification and classes satisfying the class specification were described as coalgebras. Each object belonging to a class was viewed as an element of the state space of the class, as coalgebras. We also used strong Monads theory and assertions respectively to give the parametric descriptions and semantic restrictions of objects' behaviors. Secondly,we further used coalgebraic bisimulation to discuss the behavioral equivalence relationships of objects with the considerations of strong Monads. Finally,we took an example to demonstrate how to use PVS tool to prove the consistence of class specification and objects' behavioral relationships.

Key words: Object oriented methods,Formal semantics,Coalgebraic methods,Strong monads.