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

A PROOF OBLIGATION GENERATOR FOR OBJECT-Z SPECIFICATION

作　　者：文志诚[1] 贾峰[1] 胡纯蓉[1] 

机构地区：[1]湖南工业大学计算机与通信学院,湖南株洲412008

出　　处：《计算机应用与软件》2010年第5期34-37,共4页Computer Applications and Software

基　　金：国家自然基金项目(60773110)

摘　　要：定理证明是一种形式化验证技术,也是形式化方法的重要组成部分,它能从形式规格说明中推理出应具备的性质与属性,从而可以对规格说明进行形式验证。Object-Z是形式规格说明语言Z的面向对象扩充,基于集合论与数理逻辑,具有严密的逻辑性,适合于精确地描述大型软件系统,并且可以对其形式规格说明进行推理。设计一个证明责任产生器,从Object-Z形式规格说明出发,按照相关规则自动抽取相应的证明责任,这些证明责任可以直接输入到已有的定理证明器Z/EVES中进行证明之。证明责任产生器起着Object-Z规格说明编辑器与证明器Z/EVES之间的桥梁作用,方便于Object-Z形式规格说明的验证。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 obligations（PO） according to rules from Object-Z specification.These proof obligations can input into the prover Z/EVES to be proven.This proof obligation generator bridges a gap between the Object-Z editor and the prover Z/EVES and the formal verification become easy.

关 键 词：OBJECT-Z Z/EVES 证明责任 形式验证 

分 类 号：TP311.52[自动化与计算机技术—计算机软件与理论]