Checking Object-Z Formal Specification with Z/EVES automatically
Qian Cheng, Zhicheng Wen · IOP Conference Series Materials Science and Engineering · 2019
Formal specifications can only be used when matching or non-colliding. In the conventional programming language, program integrity is checked at runtime. However, formal specification descriptions cannot be implemented in general. The grammar analysis and semantic checking of a tool sometimes invalidate conformance checks. Therefore, it is difficult to verify the consistency of formalization norms. In this paper, we propose a method to generate theorem proof for Object-Z norms. The purpose is to obtain clear confidence by verifying the consistency of norms. Finally, we use the theorem prover Z/EVES to analyze and verify theorems.