| 一个Object-Z规格说明的证明责任产生器 |
| |
| 引用本文： | 文志诚,贾峰,胡纯蓉.一个Object-Z规格说明的证明责任产生器[J].计算机应用与软件,2010,27(5):34-37. |
| |
| 作者姓名： | 文志诚 贾峰 胡纯蓉 |
| |
| 作者单位： | 湖南工业大学计算机与通信学院,湖南,株洲,412008 |
| |
| 基金项目： | 国家自然基金项目(60773110) |
| |
| 摘 要： | 定理证明是一种形式化验证技术,也是形式化方法的重要组成部分,它能从形式规格说明中推理出应具备的性质与属性,从而可以对规格说明进行形式验证。Object-Z是形式规格说明语言Z的面向对象扩充,基于集合论与数理逻辑,具有严密的逻辑性,适合于精确地描述大型软件系统,并且可以对其形式规格说明进行推理。设计一个证明责任产生器,从Object-Z形式规格说明出发,按照相关规则自动抽取相应的证明责任,这些证明责任可以直接输入到已有的定理证明器Z/EVES中进行证明之。证明责任产生器起着Object-Z规格说明编辑器与证明器Z/EVES之间的桥梁作用,方便于Object-Z形式规格说明的验证。
|
| 关 键 词： | Object-Z Z/EVES 证明责任 形式验证 |
A PROOF OBLIGATION GENERATOR FOR OBJECT-Z SPECIFICATION |
| |
| Wen Zhicheng,Jia Feng,Hu Chunrong.A PROOF OBLIGATION GENERATOR FOR OBJECT-Z SPECIFICATION[J].Computer Applications and Software,2010,27(5):34-37. |
| |
| Authors: | Wen Zhicheng Jia Feng Hu Chunrong |
| |
| Affiliation: | School of Computer and Communication/a>;Hunan University of Technology/a>;Zhuzhou 412008/a>;Hunan/a>;China |
| |
| Abstract: | Theorem proof,an important compositive part of formal method,is one kind of formal verification,which can reason about the characters that the formal specification should hold for formal specification.Therefore,it can verify the formal specification.Object-Z,an extension to formal specification language Z,is apt to describing large scale object-oriented software specification and can reason about the formal specification.This paper designs a proof obligation generator,which can extract relevant proof obliga... |
| |
| Keywords: | Object-Z Z/EVES Proof obligation Formal verification |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
