产生证明责任验证Object-Z规格说明的行为子类型继承

摘要：

Object-Z是形式规格说明语言Z的面向对象扩充,具有面向对象特点,适合描述大型面向对象软件规格说明.行为子类型继承是一种子类型继承,子类型对象拥有其超类对象的行为与属性,如果行为子类型对象替代其超类型对象时,运行时不会出错,经过验证过的形式规格说明不必再验证.本文对Object-Z定义了行为子类型继承,尤其我们系统地提出一个实现行为子类型继承和对规格说明产生相关证明责任的方法,其中这些证明责任可以判定形式规格说明是否按照其行为子类型方法进行开发的.最后,充分利用定理证明器Z/EVES来分析与验证所产生的证明责任.

关键词：Object-Z、面向对象、行为子类型、证明责任、形式验证

所属期刊栏目：30

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金项目60773110;湖南省教育厅科研基金项目08C284,07C234,08C286

在线出版日期：2009-06-26（万方平台首次上网日期，不代表论文的发表时间）

页数：共8页

页码：1049-1056