对象行为等价的终结共代数语义

摘要

终结共代数上的互模拟是等价关系,这一性质为对象的行为等价提供了一种基于共归纳原理的证明方法.首先,利用共代数给出面向对象方法中的抽象类、类和对象的形式化描述,其中抽象类被定义为一个包含方法和断言声明的类规范,类被定义为满足类规范的共代数,类的各个对象看成是共代数状态空间上的元素,而对象中方法的各种行为结构则通过强Monads进行参数化描述；接着,利用类规范的终结共代数给出对象行为等价关系的证明方法以及在各种不同Monads结构下的终结共代数语义；最后,通过实例说明如何利用PVS工具对研究结果进行验证.%The equality characteristics of bisimulations on final coalgebras entail a proof method for behavioral equality of objects based on coinductive principles. Firstly, we used coalgebras to give formal descriptions about abstract classes, classes and objects in object oriented methods, where abstract class was defined as a class specification including declarations of methods and assertions, 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. Various behavioral structures of methods in objects were described parametrically by strong Monads. Secondly,we used final coalgebras of class specification to give a proof method for objects' behavioral equality and their final coalgebraic semantics under the conditions of different Monads. Finally, some examples were employed to demonstrate how to use PVS tools for verifications.