Chicago Journal of Theoretical Computer Science

CJTCS Special Issue: CATS 2009

Selected papers from

2009 Computing: The Australasian Theory Symposium

held in Wellington, New Zealand January 20-23 2009.

Guest Editors: Rod Downey, Victoria University of Wellington, NZ

Prabhu Manyem, Shanghai University, PRC.

Article 2010-9

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

Transformation Rules for Z

Mark Utting
Department of Computer Science
The University of Waikato, New Zealand,
Petra Malik
School of Engineering and Computer Science
Victoria University of Wellington, New Zealand
Ian Toyn

June 22, 2010

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.

DOI: 10.4086/cjtcs.2010.009

[] Special Issue, CATS 2009, Article 5 [] Article 7
[back] Special Issue [back] Published articles
[CJCTS home]