Logo image
Back
Transformation rules for Z
Conference paper   Peer reviewed

Transformation rules for Z

Mark Utting, P Malik and I Toyn
Proceedings of the 15th Computing: Australasian Theory Symposium, Vol.94, pp.73-82
Computing: Australasian Theory Symposium (CATS), 15th (Wellington, New Zealand, 20-Jan-2009–23-Jan-2009)
Australian Computer Society Inc.
2009
url
http://dl.acm.org/citation.cfm?id=1862785View
Webpage

Abstract

manipulation tools preprocess reasoning engine reasoning rules schema calculus schema expressions transformation rules animation calculations semantics computation theory
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 denes 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. © 2009, Australian Computer Society, Inc.

Details

Metrics

464 Record Views
Logo image