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

被引：1

作者：

余珊珊 ^{[1
]}

李师贤 ^{[1
]}

苏锦钿 ^{[2
]}

机构：

[1] 中山大学信息科学与技术学院

[2] 华南理工大学计算机科学与工程学院

来源：

计算机科学 | 2012年 / 39卷 / 02期

基金：

广东省自然科学基金;

关键词：

对象; 行为等价; 共代数方法; 终结共代数; 强Monads;

D O I：

暂无

中图分类号：

TP301.2 [形式语言理论];

学科分类号：

080201 [机械制造及其自动化];

摘要：

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

引用

页码：179 / 182+190 +190

页数：5