This XML schema defines XML markup for formal
specifications written in the ISO Standard Z notation.
$Id: Z_1_1.xsd 5487 2007-05-10 05:01:19Z petramalik $
Copyright 2003 Mark Utting
This file is part of the Community Z Tools (CZT) project.
The CZT project contains free software; you can
redistribute it and/or modify it under the terms
of the GNU General Public License as published by
the Free Software Foundation; either version 2 of
the License, or (at your option) any later version.
The CZT project is distributed in the hope that it
will be useful, but WITHOUT ANY WARRANTY; without
even the implied warranty of MERCHANTABILITY or
FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General
Public License along with CZT; if not, write to the
Free Software Foundation, Inc., 59 Temple Place,
Suite 330, Boston, MA 02111-1307 USA
Schema negation
Schema precondition
Note: the SchText should contain just several x==Expr, and no predicate.
This means unnecessary parentheses surrounded the annotated element
Abstract: replacable by any Z base type
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
Multidigit strokes are not allowed
Supertype of all expressions
Supertype of unary expressions
Supertype of binary expressions
Supertype of binary schema operators
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 all quantifier-like expressions
Abstract subtype of QntExpr, with compulsory Expr (currently this schema does not check that the Expr is compulsory, but code should)
The mixfix attribute distinguishes
S \fun T (mixfix=true) from (_ \fun _) [S, T] (mixfix=false).
The mixfix attribute distinguishes
m + n (mixfix=true) from (_ + _)(m, n) (mixfix=false).
Supertype of all predicates
Supertype of binary predicates
Supertype of all quantifier-like predicates
The mixfix attribute distinguishes
m = n (mixfix=true) from (m,n) \in (_ = _) (mixfix=false).
Supertype of all annotations
Location annotations define the source-code location of a construct.
Section-Type environments map names to (SectionName,Type) pairs
Type annotations give the type of an expression/term
Type environments map names to types
Supertype of all Z base types