A calculus for schemes in Z

Journal article

The popularity and flexibility of the Z notation can largely be attributed to its notion of schemas. We describe these schemas and illustrate their various common uses in Z. We also present a collection of logical laws for manipulating these schemas. These laws are capable of supporting reasoning about the Z schema calculus in its full generality. This is demonstrated by presenting some theorems about the removability of schemas from Z specifications, together with outline proofs. We survey briefly models against which this logical system may be proven sound, and other related logics for Z. © 2000 Academic Press.

Authors: Brien, S; Martin, A

• Publication status: Published
• Journal: JOURNAL OF SYMBOLIC COMPUTATION
• Volume: 30
• Issue: 1
• Pages: 63-91
• Publication date: 2000-07-01
• DOI: 10.1006/jsco.1999.0347
• ISSN: 0747-7171
• Language: English