Zoy

Zoy is a (prototype of the) Z to Alloy translator described in [1] and implemented using Stratego/XT.

Motivation

The first version of the Z to Alloy translator has been implemented in Java as an extension of CZT: the CZT abstract syntax tree for Z is traversed thereby creating an abstract syntax tree for Alloy, which is then pretty-printed. However, this low-level approach is tedious to implement and yields code that is difficult to read, maintain, and reuse. The problem is that the core ideas of the abstract transformations are hidden in the low-level code needed to manipulate syntax trees. This problem has been identified before and is addressed for endogenous transformations of the Z notation by ZRules [2], an extension of Z that allows transformation rules to be written in a Z-like notation. Zoy is motived by the desire to be able to describe exogenous transformations from Z to other notations like Alloy in a similar declarative and high-level style.

Implementation

Downloads

The source for Zoy can be downloaded from the mercurial repository using the following command:

$ hg clone http://homepages.ecs.vuw.ac.nz/~petra/zoy

Installation

  1. Install Stratego/XT 0.17.

  2. Get the source for Zoy as described above.

  3. Change into the zoy directory.

  4. Run the bootstrap script followed by the configure script followed by make. This should build all the necessary parsers, pretty-printers, and transformers.

  5. Run the shell script build to adapt the generated pretty-print table to produce nicer looking output. The build script also generates a program called parenthesize that adds parenthesis if necessary and should be run on an aterm before it is printed.

  6. Run the shell script czt2alloy to translate Z to Alloy. This exploits the CZT parser and typechecker so make sure to download czt.jar and put it into the zoy directory. To run czt2alloy, provide the name of the file to be transformed like in:

    $ ./czt2alloy examples/sue.tex

  7. Alternatively, the shell script run uses Zoy's (incomplete) parser and typechecker. Provide the file to be translated to Alloy (containing Unicode markup) as an argument. The result is written to stdout.

    $ ./run examples/example.utf8

Troubleshooting

The Z grammar as well as the Z example files use Unicode characters. The default encoding on my computer is utf8 and it just works out of the box. I am not sure what needs doing on computers with a different default encoding.

Extending Zoy

The current translator doesn't handle Z schemas since a straightforward translation does not preserve semantics (see [1] for details). This section explains how Zoy can be extended to handle Z schemas.

  1. The new transformation file tools/extension.str imports z2alloy and adds another Z2A rule.

  2. Its corresponding meta file tools/extension.meta tells Stratego/XT which parser to use.

  3. The program needs to be added to Makefile.am so it gets compiled.

  4. Compile and run (as described in the shell script run but using the new program extension instead of czt2alloy now).

TODO List/Limitations

Publications

  1. Petra Malik, Lindsay Groves, Clare Lenihan. Translating Z to Alloy. Abstract State Machines, Alloy, B and Z, Second International Conference, ABZ 2010, Orford, QC, Canada, February 22-25, 2010, pp377 - 390, ©Springer. [Online Access]

  2. Mark Utting, Petra Malik, Ian Toyn. Transformation Rules for Z. Chicago Journal of Theoretical Computer Science. Volume 2010, Number 6. [Download]

Last modified: Feb 2011