Community Z Tools

by Petra Malik and Mark Utting

The Community Z Tools plugin displays a dockable window listing important Z characters and Z constructs, plus several buttons for running the CZT tools. The plugin currently supports two markup formats for Z: the LaTeX markup and the Unicode markup.

You can simply click on a Z character or construct to insert it into your current buffer, using the currently selected markup. The top line ("Paragraphs") inserts complete Z paragraphs, with uppercase placeholders for the parts that you should fill in, while most of the other constructs insert just one Z symbol or operator. For example, clicking on "Sch[]", with LaTeX markup selected, will insert a generic schema construct, like this:

  \begin{schema}{NAME}[ TYPE ]
    DECLS
  \where
    PREDS
  \end{schema}

The combo box at the left top corner of the plugin allows you to choose which markup you wish to use. This is initialized to "LaTeX Markup" each time you start jEdit, but you can change the markup at any time using this combo box. The usual goal is to set it to reflect the contents of the buffer you are editing. Your choice of markup has two effects:

1. It determines which kind of markup (LaTeX macros, or Unicode characters) is inserted into the current buffer when you click on a Z construct in the CZT plugin.
2. It determines which markup will be assumed by the CZT tools when you click the Typecheck buttons or the other buttons. WARNING: if you select "Unicode Markup", but then open a LaTeX specification and typecheck it, it will be parsed under the assumption that it contains Unicode markup, so all LaTeX constructs will be treated as informal narrative. To alert you to your mistake, the warning "No Z constructs found" will be displayed in this case.

The "Typecheck" button parses and typechecks the file in the current buffer. It always uses the file contents, rather than the current buffer contents. If the current buffer contains unsaved changes, you will be asked whether you want to continue. Saying "Yes" will continue with the parsing using the on-disk version, which will not contain your unsaved changes. Saying "No" stops the parsing and allows you to save the buffer. The result of the typechecking is displayed in the jEdit status bar. Any errors can be viewed using the ErrorList plugin.

The other two buttons in the CZT plugin convert the file in the current buffer into other markup formats. The specification can be converted to Unicode if LaTeX markup is chosen (or into LaTeX if Unicode markup is chosen), or can be translated into ZML -- XML markup for Z. If parsing and translating was successful, a new temporary buffer containing the output of the conversion is opened. In case of an error, the error list can be consulted.

Hints:

• To write the name of a primed variable, like x', use the ' character from the "Schemas" line of the CZT plugin. (In LaTeX, this just inserts the normal ASCII prime character, but in Unicode it inserts a special prime symbol. To prime a schema or expression, you must put a space inbetween the schema name and the prime. This space must be a normal space character in Unicode markup, but a special spacing command like tilde (~) in LaTeX markup.
• In LaTeX markup, you must write underscores as \_, newlines as \\ and spaces as ~. In Unicode markup these can just be written as normal ASCII characters.
• To enter subscripts within a name, use the "subscript-1" construct at the end of the "Schemas" line. This can also be used to convert "exists" into "exists-unique", or "nat" into "nat_1" etc.
• To enter superscripts within a name, use the "Transitive Closure" construct from the "Relations" line, then replace the + by the superscript that you want.
• Be careful to distinguish between some pairs of operators that look quite similar:
  • Binary subtraction (long minus) versus unary negation (short minus).
  • Set subtraction looks like a normal backslash (\) but is different (it is bolder and more sloped). The schema hiding operator is also visually similar, but is even larger and bolder.
  • The union and intersection operators come in a small binary version (for "a union b") as well as a large distributed version (for "union S", where S is a set of sets).
  • The "Relational Inverse" operator looks like a normal ASCII tilde, except that it is higher.
  • Z uses three different semicolon characters! The normal ASCII semicolon can be used as a separator between declarations, or as a separator between predicates. A larger semicolon with holes in it is used for composition of two relations (see the "Relations" line of the CZT plugin). A huge bold semicolon with holes in it is used for sequential composition of schemas (see the "Schemas" line of the CZT plugin).