This XML schema defines XML markup for formal specifications written in the ISO Standard Z notation. $Id: Z_1_4.xsd 5487 2007-05-10 05:01:19Z petramalik $ Copyright (C) 2003, 2004, 2005 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). This contains a list of at least two Oper elements. In fact, Oper has two subtypes (Operand and Operator) and the list must alternate between these. In other words, every Operand must be followed by an Operator (unless it is the last element in the list) and every Operator must be followed by an Operand (unless it is the last in the list). For example, an infix operator like '+' would be defined by Operand, Operator with Word="+", Operand. A latex markup paragraph. This paragraph contains a list of latex marku-up directives (A.2.3). 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 + T. In this case, Mixfix=true, the first (left) expression is the name, (" _ + _ "), (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 either 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) or an equality and the the second (right) Expr must be a set expression containing exactly one expression. For example, the input "m < n" generates a MemPred element with mixfix=true, left=(m,n) and right=" _ < _ ", whereas "(m,n) \in (_ < _)" 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 (3.14). It is a function from names to types, but the class just contains 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.

A latex markup directive. This is used to represent %%Zchar and %%Zword directives used in latex markup (A.2.3). The Command contains the complete latex command, including the leading backslash, whereas Unicode contains the corresponding unicode representation. The attribute is used to distinguish the kind or type of directive, for instance whether it was a %%Zinchar, which corresponds to type "NONE", or %%Zinword in which case the type is "IN".

Note that there is no unique tranlation back to a latex markup directive in latex since there could be several latex strings representing a unicode string. However, if one does want to translate back into latex markup directives, then directives with a single unicode character should be translated into the various %%Z...char commands and all other directives should be translated into %%Z...word commands (after translating each unicode character into a latex command).

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 signature annotation. It gives the signature (the global declarations) of a paragraph. 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. An abstract type which can occur in other types. A generic 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. If the List attribute is false, then this operand represents a single expression (written as an underscore). If the List attribute is true, then this operand represents a comma-separated list of expressions (written as a pair of commas). Supertype of all ANNOTATED Z constructs.