一个Object-Z规格说明的证明责任产生器

• 作者: 文志诚 胡纯蓉 贾峰
• 来源期刊: 计算机应用与软件
• 学科: 工学
• 关键词: Object-Z Z/EVES 证明责任 形式验证
• 年，卷（期）: 2010,（5）
• 所属期刊栏目: 基金项目论文
• 页码范围: 34-37
• 分类号: TP3
• 字数: 2637字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-386X.2010.05.011

摘要

定理证明是一种形式化验证技术,也是形式化方法的重要组成部分,它能从形式规格说明中推理出应具备的性质与属性,从而可以对规格说明进行形式验证.Object-Z是形式规格说明语言Z的面向对象扩充,基于集合论与数理逻辑,具有严密的逻辑性,适合于精确地描述大型软件系统,并且可以对其形式规格说明进行推理.设计一个证明责任产生器,从Object-Z形式规格说明出发,按照相关规则自动抽取相应的证明责任,这些证明责任可以直接输入到已有的定理证明器Z/EVES中进行证明之.证明责任产生器起着Object-Z规格说明编辑器与证明器Z/EVES之间的桥梁作用,方便于Object-Z形式规格说明的验证.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	贾峰	湖南工业大学计算机与通信学院	3	40	2.0	3.0
2	文志诚	湖南工业大学计算机与通信学院	49	279	10.0	14.0
3	胡纯蓉	湖南工业大学计算机与通信学院	6	32	3.0	5.0