Properties of Z specifications
- 1 July 1989
- journal article
- Published by Association for Computing Machinery (ACM) in ACM SIGSOFT Software Engineering Notes
- Vol. 14 (5) , 43-54
- https://doi.org/10.1145/71633.71634
Abstract
In this paper we show how to calculate properties of specifications written in the Z notation. In particular, we show how the precondition of an operation may be derived using rewrite rules and an application-oriented theory. As an example, we take part of the specification of an industrial-sized problem. If proofs are conducted at the level of the schema , then the structure of the proof follows the structure of the specification, and the technique scales up for verification in the large.Keywords
This publication has 1 reference indexed in Scilit:
- Software Engineering MathematicsPublished by Taylor & Francis ,1988