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.
|Cite as: Utting, M., Malik, P. and Toyn, I. (2009). Transformation Rules for Z. In Proc. Fifteenth Computing: The Australasian Theory Symposium (CATS 2009), Wellington, New Zealand. CRPIT, 94. Downey, R. and Manyem, P., Eds. ACS. 71-80. |
(local if available)