Published by Dept. CS U. Chicago. Copyright 2010 CJTCS and the author.

Abstract

Z is a formal specification language combining typed set theory, predicate calculus, and a schema calculus. This paper describes an extension of Z that allows transformation and reasoning rules to be written in a Z-like notation. This gives a high-level, declarative, way of specifying transformations of Z terms, which makes it easier to build new Z manipulation tools. We describe the syntax and semantics of these rules, plus some example reasoning engines that use sets of rules to manipulate Z terms. The utility of these rules is demonstrated by discussing two sets of rules. One set defines expansion of Z schema expressions. The other set is used by the ZLive animator to preprocess Z expressions into a form more suitable for animation.

• The article: PDF (249,134 bytes)
• Source materials: ZIP (69,415 bytes)
• Self citation in BIBTeX (205 bytes)
• Original version: PDF (200,948 bytes)

© 2010 Mark Utting, Petra Malik and Ian Toyn
Licensed under a Creative Commons Attribution License

Special Issue, CATS 2009, Article 5

Article 7

Special Issue

Published articles