This XML schema defines XML markup for formal specifications written in the ISO Standard Z notation. $Id: Z.xsd 5169 2007-02-27 21:58:05Z petramalik $ Copyright (C) 2003, 2004, 2005, 2006, 2007 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 mark-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 name. A Z name. An abstract numeral. A Z numeral. 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 binary schema expression. The type of both arguments is a set of bindings. 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). It contains a list of declarations. The restriction to ConstDecls is not validated by the schema, but code should check. 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 and explicit are always true, and the list of instantiating expressions is non-empty (it contains [S,T]).
  • C.6.28 (Reference). For example: \arithmos In this case, mixfix and explicit are always false and the list of instantiating expressions is empty. Another example before typechecking is \emptyset. The typechecker transforms \emptyset to a generic instantiation and explicit remains false (see 13.2.3.3).
  • C.6.29 (Generic Instantiation). For example: \emptyset[T]. In this case, mixfix is always false and the list of instantiating expressions is non-empty (it contains [T]). The explicit attribute indicates whether the instantiating expressions are explicitly given in the specification (explicit is true) or whether they were inferred by the typechecker (explicit is false).
 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). The schema does not check that the NameList is non-empty, but code should. 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). The schema does not check that the RenameList is non-empty, but code should. A binding construction expression (C.6.27). A tuple selection expression (C.6.26). The schema does not check that the numeral is positive, but code should. 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 paragraph list. A paragraph list. An abstract expression list. An expression list (12.2.12). An abstract rename list. A rename list. An abstract name list. A name list. An abstract branch list. A branch list. An abstract freetype list. A freetype list. An abstract predicate (C.5). An abstract superclass for constant true/false facts. An abstract binary predicate. An abstract quantifier like predicate. A schema predicate. A relation operator application (C.5.12).
  • Membership predicate. In this case, Mixfix=false, the first (left) expression is the element, and the second (right) expression is the set. For example, "n \in S" has left="n" and right="S".
  • Equality. In this case, Mixfix=true, the first (left) expression is the left-hand side of the equality, and the second (right) expression is a singleton set containing the right-hand side of the equality. For example: "n = m" has left="n" and right="{m}".
  • Other operator application. In this case, Mixfix=true, the first (left) expression is usually a tuple containing the corresponding number of arguments, and the second (right) expression is the operator name. However, for a unary operator, the left expression does not have to be a tuple. For example, "n < m" has left="(n,m)" and right=" _ < _ ", "disjoint s" has left="s" and right="disjoint _ ", and if foo was declared as a unary postfix operator, then "(2,3) foo" would have left= "(2,3)" and right=" _ foo".
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 And 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). An abstract schema text (C.7). A schema text (C.7). An abstract declaration list (12.2.7.2). A declaration list (12.2.7.2). An abstract stroke list. A stroke list. The parents of a section. A free type (C.4.10). The schema does not check that the FreetypeList is non-empty, but code should. A branch of a free type (C.4.10). 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 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).

This empty class is the base class for all 'official' annotations -- those defined for standard Z and the various extensions of standard Z. This gives us the ability to add attributes to all such annotations in the future. However, note that the Anns list within each Term object is not limited to just the subclasses of Ann -- arbitrary objects are allowed, so that new kinds of annotations can be added without having to define them in an XML schema etc. Location annotations define the source-code location of a construct. The Line and Col numbers, if present, refer to an identifying token within the construct, such as the equality token of an equality predicate, or the opening brace of a set comprehension. The Line and Col numbers start from (0,0), so may need adjusting to give correct positions in various editors. The Start number, if present, gives the position of the start of the construct from the beginning of the document (0 means the first character of the document), and the Length number gives the number of characters from the beginning of the construct to the end. The Length may be zero if the construct exists in one markup, but is not visible in another markup. 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. 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 constructs.