Conference paper
Transformation Rules for Z
Chicago Journal of Theoretical Computer Science, 9
Computing: The Australasian Theory Symposium (CATS), 15th (Wellington, New Zealand, 20-Jan-2009–23-Jan-2009)
M I T Press
2010
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.
Details
- Title
- Transformation Rules for Z
- Authors
- Mark Utting (Author) - University of Waikato, New ZealandPetra Malik (Author) - University of Waikato, New ZealandIan Toyn (Author)
- Publication details
- Chicago Journal of Theoretical Computer Science, 9; 26
- Conference details
- Computing: The Australasian Theory Symposium (CATS), 15th (Wellington, New Zealand, 20-Jan-2009–23-Jan-2009)
- Publisher
- M I T Press
- Date published
- 2010
- DOI
- 10.4086/cjtcs.2010.009
- ISSN
- 1073-0486
- Copyright note
- Copyright © 2010 Mark Utting, Petra Malik and Ian Toyn Licensed under a Creative Commons Attribution License.
- Organisation Unit
- School of Science and Engineering - Legacy; University of the Sunshine Coast, Queensland
- Language
- English
- Record Identifier
- 99448819702621
- Output Type
- Conference paper
Metrics
247 File views/ downloads
587 Record Views