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

• Alloy SDF grammar thanks to Shannon Bay

• Z SDF grammar

• Transformations

  The most important transformations are:

  • z2alloy.str contains the Z to Alloy transformations as defined in [1].
  • lib/z/syntax_transformation_rules.str contains desugaring (syntax transformation) rules as defined in the ISO Z Standard.
  • lib/z/typecheck.str defines (a very limited set of) Z typecheck rules.

  Note that brackets based on the %-character delimit Z notation; @ is used to delimit Alloy. A letter indicates the sort of the Z or Alloy construct; P is used for predicates, E is used for expressions, etc. A tilde is used as an escape mechanism that allows the use of Stratego syntax within Z and Alloy formulas. These conventions are defined in MetaZ.sdf and StrategoAlloy.sdf

Downloads

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

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

• The Z that can be parsed is rather restricted and no useful error messages are provided when parse errors occur.
  • Only Unicode mark-up (UTF8) is supported. CZT can be used to translate to and from other mark-ups.
  • Declarations must be separated by semicolon (just putting declaration on a new line is not supported yet). This means that when CZT is used to translate from LaTeX to Unicode, the semicolons need to be added by hand (since I don't think CZT has an option to separate declarations using semicolon when printed).
  • Only simple names (containing alphanumerical characters and numbers) can be parsed. Handling of strokes and other fancy things is not implemented yet.
  • No toolkits exist so most of the common operators and definitions cannot be used.
• Typechecking Z (typecheck information is required for the transformations to Alloy to work properly): Only a few typecheck rules have been implemented so far. Implementing a full blown typechecker in Stratego/XT is probably a lot of work. I am currently investigating whether the CZT typechecker can be exploited.
• The Z constructs that can be translated to Alloy are defined in [1]. Note that Z schemas, for example, cannot be translated. Also, section headers (and thus declaring dependencies between Z sections via parents) are completely ignored.

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]