This XML schema defines XML markup for formal specifications written in the ISO Standard Z notation. $Id: Z_1_2.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 A specification (C.2). An abstract section. A concrete section (C.3). Note that it may contain unparsed paragraphs. A completely unparsed section. It is used for representing possibly erroneous specifications. It may become one or more sections if it can be parsed. Narrative before or after sections. An abstract paragraph (C.4). A (generic) axiomatic paragraph, (generic) schema definition, or (generic) horizontal definition (C.4.3, C.4.4, C.4.5, C.4.6, C.4.7, C.4.8). A (generic) conjecture paragraph (C.4.11, C.4.12). A free types paragraph (C.4.10). A given types paragraph (C.4.2). A narrative paragraph. It contains arbitrary unicode and markup. An operator template paragraph (C.4.13). A completely unparsed paragraph. An abstract declaration. A constant declaration (C.7). Example: x==3. An include declaration (C.7). Example: \Delta S A variable declaration (C.7). Example: a,b:T An abstract Z name that can be decorated. A declaring name. A referencing name. The Decl attribute of type IDREF points to the matching declaration, which may not be the nearest enclosing one. An abstract stroke. The stroke "?". The stroke "!". The stroke "'". A digit stroke. Note that multidigit strokes are not allowed. An abstract expression (C.6). An abstract unary expression. An abstract binary expression. An abstract expression containing 0..N expressions. An abstract expression containing 2..N expressions. Currently the schema does not check that there are at least two expressions, but code should. An abstract quantifier-like expression. An abstract quantifier-like expression with compulsory expression. Currently the schema does not check that the Expr is compulsory, but code should. A binding extension expression (C.6.35). A conditional expression (C.6.13). A number literal expression (C.6.30). A reference expression (C.6.21, C.6.28, C.6.29).

• C.6.21 (Generic Operator Application). For example: S \rel T. In this case, mixfix is always true and the list of type expressions is non-empty (it contains [S,T]).
• C.6.28 (Reference). For example: \emptyset. In this case, mixfix is always false and the list of type expressions is empty.
• C.6.29 (Generic Instantiation). For example: \emptyset[T]. In this case, mixfix is always false and the list of type expressions is non-empty (it contains [T]).

A schema construction expression (C.6.34). A binding selection expression (C.6.25). A schema decoration expression (C.6.23). A schema hiding expression (C.6.16). A schema negation expression (C.6.12). A powerset expression (C.6.20). A schema precondition expression (C.6.18). A schema renaming expression (C.6.24). A binding construction expression (C.6.27). A tuple selection expression (C.6.26). A function application (C.6.21, C.6.22).

• C.6.21 (Function Operator Application). For example: S \cup T. In this case, Mixfix=true, the first (left) expression is the name, (_ \cup _), (that is, a RefExpr with Mixfix=false!) and the second (right) expression is (S,T).
• C.6.22 (Application). For example: \dom R. In this case, Mixfix=false, the first (left) expression is the function, \dom, (again, a RefExpr with Mixfix=false) and the second (right) expression is the argument R.

As another example, m + n has Mixfix=true, whereas (_ + _)(m, n) has Mixfix=false. A schema composition expression (C.6.14). A schema piping expression (C.6.15). A schema projection expression (C.6.17). A schema conjunction expression (C.6.11). A schema disjunction expression (C.6.10). A schema implication expression (C.6.9). A schema equivalence expression (C.6.8). A set extension expression (C.6.31). A Cartesian product expression (C.6.19). A tuple extension expression (C.6.36). A (characteristic) definite description expression (C.6.6, C.6.37). A (characteristic) set comprehension expression (C.6.32, C.6.33). A schema existential quantification (C.6.3). A schema unique existential quantification (C.6.4). A schema univeral quantification expression (C.6.2). A function construction expression (C.6.5). A substitution expression (C.6.7). Note that the SchText should contain x==Expr only, and no predicate. An abstract predicate (C.5). An abstract binary predicate. An abstract quantifier like predicate. A schema predicate. A relation operator application (C.5.12). The mixfix attribute is false iff the input has the form Expr1 \in Expr2. When mixfix=true, the second (right) Expr must be a relational operator and the first (left) Expr must be a tuple containing the corresponding number of arguments (unless the operator has one argument, then no tuple is required). For example, the input "m \leq n" generates a MemPred element with mixfix=true, left=(m,n) and right=" _ \leq _ ", whereas "(m,n) \in (_ \leq _)" has the same left and right expressions, but mixfix=false. A negation (C.5.11). Falsity (C.5.15). Truth (C.5.14). A conjunction (C.5.5, C.5.6, C.5.10). The Op attribute identifies the kind of conjunction: whether it is an /\, a semicolon, a newline, or a chain (an implicit conjunction like in a=b=c). An implication (C.5.8). An equivalence (C.5.7). A disjunction (C.5.9). An existential quantification (C.5.3). An unique existential quantification (C.5.4). An universal quantification (C.5.2). The parents of a section. A free type (C.4.10). A branch of a free type (C.4.10). A schema text (C.7). A signature. It is a function from names to types, but the class just containes a list of pairs consisting of a name and a type. A pair of a name and an expression. A pair of two names. A pair of a name and a type. A tuple consisting of a name, a section, and a type. Location annotations define the source-code location of a construct. This means unnecessary parentheses surrounded the annotated element A section-type environment (4.4 Table 22). It associates names of declarations with the name of the ancestral section that originally declared the name paired with its type. A type annotation. It gives the type of an expression/term. A type environment (4.4 Table 22). It associates names with types. An abstract base type. A generic parameter type. A given type. A powerset type. A Cartesian product type. A schema type. Abstract parent of Operator/Operand. An Operator Token, used within an Operator Template. An Operator Argument, used within an Operator Template. Supertype of all ANNOTATED Z constructs.