Package net.sourceforge.czt.parser.z

Provides classes for parsing Z specifications written in unicode or using LaTeX mark-up as defined in the ISO Standard for Z.

See:
Description

Interface Summary

LatexMarkupParser.LatexLexer

Class Summary

ContextFreeScanner	The context-free lexer for Z specifications in unicode format.
KeywordScanner	This is a keyword lexer (part of context-sensitive lexis) for Z specifications in unicode format.
Latex2Unicode	The low-level latex to unicode scanner for Z.
LatexMarkupParser	A latex markup parser that looks like a scanner.
LatexParser	A parser for LaTeX mark-up.
LatexScanner	A latex scanner for Z specifications.
LatexToUnicode	The high-level latex to unicode converter for Z .
NewlineScanner	This is a NL lexer (part of context-sensitive lexis) for Z specifications in unicode format.
OperatorScanner	This is an operator lexer (part of context-sensitive lexis) for Z specifications in unicode format.
Parser	CUP v0.11a beta 20060608 generated parser.
ParserState	A class recording parser state related information.
ParseUtils	Utilities for parsing Z specifications.
Sym	CUP generated class containing symbol constants.
SymMap
UnicodeParser	A parser for unicode.
UnicodeScanner	A scanner for lexing Z specifications in unicode format.
ZParseError	A Z parse error.
ZParseResourceBundle

Enum Summary

Keyword
TokenName	An enumeration of Z tokens.
ZParseMessage	An enumeration of possible parse/scan messages, warnings, and errors that may occur during a parse.

Package net.sourceforge.czt.parser.z Description

Provides classes for parsing Z specifications written in unicode or using LaTeX mark-up as defined in the ISO Standard for Z. The overall structure of the parser is shown in the following picture:

The UnicodeParser is responsible for parsing Z specifications written in unicode. It consists of an LARL Parser, which gets its input from the UnicodeScanner.

According to the ISO Standard for Z, the lexis for Z specifications consists of two phases: the context-free lexis and the context-sensitive lexis. The ContextFreeScanner is an implementation of the context-free lexis described in section 7.2 of the Standard. The context-free lexis is followed by the context-sensitive lexis provided by KeywordScanner and OperatorScanner. The SmartScanner resolves some ambiguities in the grammer.

The LatexParser parses Z specifications in LaTeX. This is done by first converting the latex mark-up into unicode. Then the UnicodeParser is used to parse the specification. The CztReader is responsible for preserving the line and column number information of the latex document.

The result of a parse is an abstract syntax tree (AST) representation of the parsed specification. Note that the strings, like for instance operator names, used within the AST are provided in unicode independendly from the input language used (whether unicode or LaTeX).

Limitations and incompatibilities with the ISO Standard for Z:

• The parents of a section must either be already parsed (and information about it accessible via section info objects), or the sections must be provided in the right order, i.e. the parents of a section must occur before the section having these parents. This makes sure that the parser has access to the operator tables (and latex mark-up table in case LaTeX mark-up is parsed) of the parents of a section.
• User defined operator must be defined before their use. This is not standard conforming since according to the standard, the scope of an operator template is the whole section in which it appears (not only from the operator template onwards).
• (LaTeX parser only) Latex markup directives must be outside formal paragraphs. Currently they are just ignored inside formal paragraphs.
• (LaTeX parser only) Latex markup directives must be defined before their latex command is used. This is not standard conforming since according to the standard, the scope of a latex markup directive is the whole section in which it appears (not only from the operator template onwards).