一种基于共代数的面向对象形式语义  

Formal Semantics of Object Oriented Methods Based on Coalgebras

作　　者：余珊珊[1] 李师贤[1] 苏锦钿[2] 

机构地区：[1]中山大学信息科学与技术学院,广州510275 [2]华南理工大学计算机科学与工程学院,广州510640

出　　处：《计算机科学》2011年第8期142-146,共5页Computer Science

基　　金：国家自然科学基金资助项目(60673122);广东省自然科学基金资助项目(8151030007000002)资助

摘　　要：针对面向对象方法的数学理论基础相对薄弱的问题,利用共代数方法从范畴论及观察的角度研究面向对象的形式语义及行为关系。首先,给出类和对象的共代数描述,其中抽象类定义成一个类规范,类定义为满足类规范的共代数,类的各个对象则看成共代数状态空间上的元素,并分别利用强Monads理论和断言给出方法的行为的参数化描述和语义约束;接着,利用共代数互模拟探讨了不同对象在强Monads下的行为等价关系;最后用实例说明如何通过PVS工具证明类规范的一致性及对象的行为关系。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.

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

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]