Checking Object-Z Formal Specification with Z/EVES automatically

2nd International Symposium on Application of Materials Science and Energy Materials

材料科学;能源学

Cheng, Qian^1 ; Wen, Zhicheng^1

College of Computer Science, Jiangxi University of Engineering, Xinyu, Jiangxi Province

338000, China^1

关键词: Object Z;    Runtimes;    Theorem provers;   

Others  :  https://iopscience.iop.org/article/10.1088/1757-899X/490/4/042016/pdf
DOI  :  10.1088/1757-899X/490/4/042016

学科分类：材料科学（综合）

来源: IOP

【 摘 要 】

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.