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

计算机科学 ›› 2012, Vol. 39 ›› Issue (2): 183-186.

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

余珊珊，李师贤，苏锦宝田

(中山大学信息科学与技术学院广州 510275)，(华南理工大学计算机科学与工程学院广州 510640）

出版日期:2018-11-16 发布日期:2018-11-16

Final Coalgebraic Semantics for Behavioral Equality of Objects

Online:2018-11-16 Published:2018-11-16

摘要/Abstract

摘要： 终结共代数上的互模拟是等价关系，这一性质为对象的行为等价提供了一种基于共归纳原理的证明方法。首先，利用共代数给出面向对象方法中的抽象类、类和对象的形式化描述，其中抽象类被定义为一个包含方法和断言声明的类规范，类被定义为满足类规范的共代数，类的各个对象看成是共代数状态空间上的元素，而对象中方法的各种行为结构则通过强Monads进行参数化描述;接着，利用类规范的终结共代数给出对象行为等价关系的证明方法以及在各种不同Monads结构下的终结共代数语义;最后，通过实例说明如何利用PVS工具对研究结果进行验证。

关键词: 对象，行为等价，共代数方法，终结共代数，强Monads

Abstract: 终结共代数上的互模拟是等价关系，这一性质为对象的行为等价提供了一种基于共归纳原理的证明方法。首先，利用共代数给出面向对象方法中的抽象类、类和对象的形式化描述，其中抽象类被定义为一个包含方法和断言声明的类规范，类被定义为满足类规范的共代数，类的各个对象看成是共代数状态空间上的元素，而对象中方法的各种行为结构则通过强Monads进行参数化描述;接着，利用类规范的终结共代数给出对象行为等价关系的证明方法以及在各种不同Monads结构下的终结共代数语义;最后，通过实例说明如何利用PVS工具对研究结果进行验证。

Key words: Objects, Behavioral equivalence, Coalgebraic methods, Final coalgebras, Strong Monads

余珊珊，李师贤，苏锦宝田. 对象行为等价的终结共代数语义[J]. 计算机科学, 2012, 39(2): 183-186. https://doi.org/

参考文献

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed