Back to Search
Start Over
Checking the consistency of Object-Z formal specification based on theorem proof.
- Source :
-
Journal of Computational Methods in Sciences & Engineering . 2020, Vol. 20 Issue 1, p217-226. 10p. - Publication Year :
- 2020
-
Abstract
- A software formal specification is useful if and only if it is consistent or non-conflictive. However, checking the correctness or consistency of a formal specification is a difficult task. This paper proposes a method to prove its consistency or correctness by generating relevant theorem proofs. Checking the correctness and consistency of Object-Z formal specification is the main goal, which can make the specifier to get confident. Because Object-Z has inheritance property, this paper discusses it from different aspects, and focuses on the reuse of theorem proof. Finally, theorem prover Z/EVES is used to analyze and verify the Object-Z theorem proofs (semi-)automatically. [ABSTRACT FROM AUTHOR]
- Subjects :
- *EVIDENCE
*TECHNICAL specifications
Subjects
Details
- Language :
- English
- ISSN :
- 14727978
- Volume :
- 20
- Issue :
- 1
- Database :
- Academic Search Index
- Journal :
- Journal of Computational Methods in Sciences & Engineering
- Publication Type :
- Academic Journal
- Accession number :
- 142832364
- Full Text :
- https://doi.org/10.3233/JCM-193773