This XML schema defines XML markup for formal specifications written in the ISO Standard Z notation. $Id: Z_1_0.xsd 5487 2007-05-10 05:01:19Z petramalik $ Abstract: replacable by any kind of section Concrete Z section Abstract: replacable by any paragraph Abstract: replacable by any declaration Abstract: replacable by any kind of stroke Multidigit strokes are not allowed Abstract: replacable by any expression Schema negation Schema precondition Note: the SchText should contain x==Expr only, and no predicate. Abstract: replacable by any predicate Type annotations give the type of an expression/term Type environments map names to types Section-Type environments map names to (SectionName,Type) pairs Location annotations define the source-code location of a construct. This means unnecessary parentheses surrounded the annotated element Abstract: replacable by any Z base type Supertype of ALL Z constructs Supertype of all ANNOTATED Z constructs Supertype of all sections A parsed Z section (may contain unparsed paragraphs) A completely unparsed Z section Narrative before or after sections Supertype of all paragraphs Supertype of all declarations Supertype of all Z names that can be decorated The Decl=IDREF attribute points to the matching declaration, which may not be the nearest enclosing one Supertype of the four kinds of name decorations Supertype of all expressions Supertype of unary expressions Supertype of binary expressions Supertype of lists of 0..N expressions Supertype of lists of 2..N expressions (currently this schema does not check that there are at least two expressions, but code should) Supertype of binary logical schema operators Supertype of all quantifier-like expressions Abstract subtype of QntExprType, with compulsory Expr (currently this schema does not check that the Expr is compulsory, but code should) Supertype of schema exists expressions Supertype of all predicates Supertype of binary predicates Supertype of all quantifier-like predicates Supertype of all annotations Supertype of all Z base types