| 产生证明责任验证Object—Z规格说明的行为子类型继承 |
| |
| 引用本文： | 文志诚,李长云,满君丰.产生证明责任验证Object—Z规格说明的行为子类型继承[J].小型微型计算机系统,2009,30(6). |
| |
| 作者姓名： | 文志诚 李长云 满君丰 |
| |
| 作者单位： | 湖南工业大学,计算机与通信学院,湖南,株洲,412008 |
| |
| 基金项目： | 国家自然科学基金，湖南省教育厅科研基金 |
| |
| 摘 要： | Object-Z是形式规格说明语言Z的面向对象扩充,具有面向对象特点,适合描述大型面向对象软件规格说明.行为子类型继承是一种子类型继承,子类型对象拥有其超类对象的行为与属性,如果行为子类型对象替代其超类型对象时,运行时不会出错,经过验证过的形式规格说明不必再验证.本文对Object-Z定义了行为子类型继承,尤其我们系统地提出一个实现行为子类型继承和对规格说明产生相关证明责任的方法,其中这些证明责任可以判定形式规格说明是否按照其行为子类型方法进行开发的.最后,充分利用定理证明器Z/EVES来分析与验证所产生的证明责任.
|
| 关 键 词： | 面向对象 行为子类型 证明责任 形式验证 |
Checking Behavioral Subtyping Inheritance for Object-Z Specification via Generating Proof Obligation |
| |
| WEN Zhi-cheng,LI Chang-yun,MAN Jun-feng.Checking Behavioral Subtyping Inheritance for Object-Z Specification via Generating Proof Obligation[J].Mini-micro Systems,2009,30(6). |
| |
| Authors: | WEN Zhi-cheng LI Chang-yun MAN Jun-feng |
| |
| Abstract: | |
| |
| Keywords: | Object-Z |
| 本文献已被 维普 万方数据 等数据库收录！ |
|
