This page describes an XML markup for Z, based on the ISO Z Standard (2002). See Ian Toyn's list of differences between standard Z and Spivey Z for an overview of most of the changes. The official ISO Z standard (ISO/IEC 13568:2002) is now available for free download (click on the 'Freely Available Standards' link in the left column, then search for 'Formal Specification'.

Introduction

The ZML format is specified by an XML schema file (Z.xsd). This specifies the allowable 'syntax' of each ZML construct. See the ZB2003 proceedings for a paper describing this markup.

To allow for evolution of the ZML format, each Z specification file (spec.xml) should specify which version of the ZML format it is using, by including a version="Major.Minor" attribute in the <Spec> tag. The default is the oldest version: version="1.0".

Versions of the ZML Schema

The following table shows the public versions of Z.xsd that have been released plus the official location of that schema (this can be used in the schemalocation attribute of .xml files). It also relates that public version number to the internal revision number of Z.xsd within the CZT CVS or SVN repository, and gives a summary of the significant changes from the previous version. An exhaustive list of all changes to Z.xsd (most of which do not affect the XML format) can be found in the CZT SVN repository.

Version Location SVN/CVS Rev# Changes/Comments
2.1 Z_2_1.xsd 5169 Removed XML Schema elements and types DeclName, ZDeclName, RefName, ZRefName, DeclNameList, ZDeclNameList, RefNameList, and ZRefNameList and introduce new XML Schema elements and types Name, ZName, NameList, and ZNameList instead since the distinction between DeclName and RefName does not seem to be relevant and makes handling of IDs more difficult. Name is now used in places where either a DeclName or a RefName has been used; NameList is used in places where either a DeclNameList or a RefNameList has been used.

Remove optional attributes Author, Modified, and Source from element Spec. Annotations can be used to preserve this sort of information.
2.0 Z_2_0.xsd 1.95 Renamed the SchText element and type to ZSchText and added new abstract element and type SchText. The element ZSchText is declared to be in the substitution group of (the new abstract) element SchText. This makes it possible to define new kinds of schema texts by providing new elements that are in the substitution group of SchText like, for example, jokers (metavariables) as used in Cadiz's tactic language.

Renamed the DeclName element and type to ZDeclName and added new abstract element and type DeclName. The element ZDeclName is declared to be in the substitution group of (the new abstract) element DeclName.

Renamed the RefName element and type to ZRefName and added new abstract element and type RefName. The element ZRefName is declared to be in the substitution group of (the new abstract) element RefName.

Deleted abstract element and type Name since it is no longer used.

Added new element and type Numeral (abstract) and ZNumeral and use it in NumExpr and TupleSelExpr.

Added new elements and types for lists: BranchList (abstract) and ZBranchList, DeclList (abstract) and ZDeclList, DeclNameList (abstract) and ZDeclNameList, ExprList (abstract) and ZExprList, FreetypeList (abstract) and ZFreetypeList, ParaList (abstract) and ZParaList, RefNameList (abstract) and ZRefNameList, RenameList (abstract) and ZRenameList, StrokeList (abstract) and ZStrokeList. Those are now used instead of sequences defined via minOccurs and maxOccurs elements.

Removed element and type NameExprPair since it is not used any more.

Removed element and type TypeEnvAnn since it is not used. Use Signature instead.

Rename NameNamePair as NewOldPair and use Z ordering of the names.

Rename Number as Digit to distinguish it from Numeral.

Rename type TermA as Term and let all other types extend from Term. Now all elements can have annotations.

Added new attribute Explicit to RefExpr. It is used to distinguish whether the instantiating expressions are explicitly given in the specification (explicit is true) or whether they were inferred by the typechecker (explicit is false).

Added new element/type Ann, an abstract base class for all annotations. This is mostly for consistency with our other complex type hierarchies.

Added new attributes Start and Length to LocAnn.

Improve some documentation.
1.4 Z_1_4.xsd 1.71 Added new elements/types for SignatureAnn to be used by the typechecker.
1.3 Z_1_3.xsd 1.69 Added new elements/types LatexMarkupPara and Directive to support storing the latex markup function in the AST.

Added new elements/types GenericType and Type2 to reflect the grammar for types given in the ISO Standard for Z.

Renamed GenType to GenParamType to avoid confusion with GenericType.

Changed attribute Loc in LocAnn to be optional.

Changed attribute Prec in OptempPara to be optional. This can be used by, for instance, prefix templates, which do not have a precedence value.

Remove the default value for the Assoc attribute. Not setting this attribute can be used by, for instance, prefix templates, which do not have an associativity.

Changed element Oper to be abstract.

Improved documentation.
1.2 Z_1_2.xsd 1.55 Changed operator templates to use an inheritance hierarchy for Operator and Operand. This is more consistent with other parts of the schema, and allows stronger typing within the Java AST. This has changed the XML format slightly from: 
<OptempPara ...>
  <Operand/>
  <Word>*</Word>
  <Operand/>
</OptempPara>
to 
<OptempPara ...>
  <Operand/>
  <Operator><Word>*</Word></Operator>
  <Operand/>
</OptempPara>
1.1 Z_1_1.xsd 1.39 Changed namespace and schemaLocation to czt.sourceforge.net

Added version/author/date/source-location attributes to <Spec>

Changed operator templates slightly, so that they now contain a (alternating) sequence of <Word> and <Operand> tags, where <Operand> may add the attribute List="true" to indicate an sequence of operands.

Renamed FreeType to Freetype to conform to the Z standard.

Added a tag around rename pairs, for consistency with other pairs and triples. Also swapped the order of NewName and OldName within these pairs, to reflect the functional nature (domain -> range) of the renaming.

Removed ##other from Section and Paragraph because it causes ambiguity when extending the schema. This makes the schema more strict, because standard XML validators will now REQUIRE Z extensions to have a schema.
1.0 Z_1_0.xsd 1.16 This version was described in the ZB2003 paper and used by several projects at the National University of Singapore.

If <Spec> has no version attribute, this version is used.

Background and Rationale

The goal of providing an XML markup for Z specifications is to make it easier for tools to exchange annotated specifications. For example, a specification might be parsed and typechecked by one tool, then passed to another tool (in XML format) which expands schema calculus and puts predicates into disjunctive normal form, then passed to another tool (in XML format) which generates test cases from each disjunct. The XML format is simply a textual representation of the annotated syntax tree of the Z specification.

Some advantages of using XML to exchange Z specifications between tools:

  • all programming languages provide libraries for loading and saving XML files, so multiple-language toolsets are easier.
  • annotations can be attached to any node of this ZML format, so it is easy to include type information for every variable and every expression.
  • each tool does not need to parse and typecheck Z -- this can be done by one tool, and the results used by many other tools.
  • there are many analysis and transformation tools for XML, such as the XSLT language which makes it easy to transform XML files into other formats.
A disadvantage is that XML files are large (at least 20 times larger than the Z specification source), which makes transfer between tools a reasonably costly operation. For this reason, CZT also offers libraries of Java classes and utilities which can directly manipulate the Z AST in memory. This allows tighter integration of tools, but is limited to tools written in Java that use our Z AST classes. So in practice, we expect that existing tools and non-Java tools will use the ZML format to transfer specifications between tools, while new Z tools written in Java using CZT will be able to directly pass AST objects from one tool to another, as well as being able to read and write them as ZML.