Generating Proof Obligation to Verify Object-Z Specification

A formal specification is usable only if it is consistent or non-conflictive. In traditional programming languages, the consistency checking for program is performed at run time. But formal specifications are not executable in general. The syntax parsing and semantics checking in certain tools are not effective for the consistency checking sometimes. Hence, it is difficult to verify the consistency of a formal specification. This paper presents an approach to generating relevant proof obligations for Object-Z specification systemically. It aims to verify the consistency of a specification developed with Object-Z, which enables the specifier to gain confidence. Because Object-Z is an object-oriented formal specification language and has inheritance characteristic, we discuss it from several aspects and take into account the reuse of proof obligation emphatically. Finally, we make use of the theorem prover Z/EVES to analyze and verify the proof obligations.