10.3969/j.issn.1002-137X.2012.02.041
对象行为等价的终结共代数语义
终结共代数上的互模拟是等价关系,这一性质为对象的行为等价提供了一种基于共归纳原理的证明方法.首先,利用共代数给出面向对象方法中的抽象类、类和对象的形式化描述,其中抽象类被定义为一个包含方法和断言声明的类规范,类被定义为满足类规范的共代数,类的各个对象看成是共代数状态空间上的元素,而对象中方法的各种行为结构则通过强Monads进行参数化描述;接着,利用类规范的终结共代数给出对象行为等价关系的证明方法以及在各种不同Monads结构下的终结共代数语义;最后,通过实例说明如何利用PVS工具对研究结果进行验证.
对象、行为等价、共代数方法、终结共代数、强Monads
39
TP301.2(计算技术、计算机技术)
国家自然科学基金项目60673122;广东省自然科学基金项目8151030007000002
2012-04-27(万方平台首次上网日期,不代表论文的发表时间)
共5页
179-182,190