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