HOL-Z 2.0: A Proof Environment for Z-Specifications
| dc.creator | Brucker,Achim | |
| dc.creator | Rittinger,Frank | |
| dc.creator | Wolff,Burkhart | |
| dc.date | 2003 | |
| dc.date.accessioned | 2024-02-06T12:52:14Z | |
| dc.date.available | 2024-02-06T12:52:14Z | |
| dc.description | We present a new proof environment for the specification language Z. The basis is a semantic representation of Z in a structure-preserving, shallow embedding in Isabelle/HOL. On top of the embedding, new proof support for the Z schema calculus and for proof structuring are developed. Thus, we integrate Z into a well-known and trusted theorem prover with advanced deduction technology such as higher-order rewriting, tableaux-based provers and arithmetic decision procedures. A further achievement of this work is the integration of our embedding into a new tool-chain providing a Z-oriented type checker, documentation facilities and macro support for refinement proofs, as a result, the gap has been closed between a logical embedding proven correct and a tool suited for applications of nontrivial size. | |
| dc.format | text/html | |
| dc.identifier | https://doi.org/10.3217/jucs-009-02-0152 | |
| dc.identifier | https://lib.jucs.org/article/27933/ | |
| dc.identifier.uri | https://openrepository.mephi.ru/handle/123456789/8293 | |
| dc.language | en | |
| dc.publisher | Journal of Universal Computer Science | |
| dc.relation | info:eu-repo/semantics/altIdentifier/eissn/0948-6968 | |
| dc.relation | info:eu-repo/semantics/altIdentifier/pissn/0948-695X | |
| dc.rights | info:eu-repo/semantics/openAccess | |
| dc.rights | J.UCS License | |
| dc.source | JUCS - Journal of Universal Computer Science 9(2): 152-172 | |
| dc.subject | theorem proving | |
| dc.subject | refinement | |
| dc.subject | Z | |
| dc.title | HOL-Z 2.0: A Proof Environment for Z-Specifications | |
| dc.type | Research Article |