1、BRITISH STANDARD BS ISO/IEC 13568:2002 Information technology Z formal specification notation Syntax, type system and semantics ICS 35.060 BS ISO/IEC 13568:2002 This British Standard, having been prepared under the direction of the DISC Board, was published under the authority of the Standards Polic
2、y and Strategy Committee on 8 August 2002 BSI 8 August 2002 ISBN 0 580 40198 7 National foreword This British Standard reproduces verbatim ISO/IEC 13568:2002 and implements it as the UK national standard. The UK participation in its preparation was entrusted to Technical Committee IST/5, Programming
3、 languages, which has the responsibility to: A list of organizations represented on this committee can be obtained on request to its secretary. Cross-references The British Standards which implement international publications referred to in this document may be found in the BSI Catalogue under the s
4、ection entitled “International Standards Correspondence Index”, or by using the “Search” facility of the BSI Electronic Catalogue or of British Standards Online. This publication does not purport to include all the necessary provisions of a contract. Users are responsible for their correct applicati
5、on. Compliance with a British Standard does not of itself confer immunity from legal obligations. aid enquirers to understand the text; present to the responsible international/European committee any enquiries on the interpretation, or proposals for change, and keep the UK interests informed; monito
6、r related international and European developments and promulgate them in the UK. Summary of pages This document comprises a front cover, an inside front cover, the ISO/IEC title page, pages ii to vi, pages 1 to 189, and a back cover. The BSI copyright date displayed in this document indicates when t
7、he document was last issued. Amendments issued since publication Amd. No. Date Comments Reference number ISO/IEC 13568:2002(E)INTERNATIONAL STANDARD ISO/IEC 13568 First edition 2002-07-01 Information technology Z formal specification notation Syntax, type system and semantics Technologies de linform
8、ation Notation Z pour la spcification formelle Syntaxe, systme de caractres et smantique BSISO/IEC13568:2002ii BSISO/IEC13568:2002Contents Page Foreword . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . v Introduction . . . . . . . . . . .
9、. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . vi 1 Scope . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 2 Normative references . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
10、. . . . . . . . . . . . 1 3 Terms and denitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 4 Metalanguages . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 5 Conformance . . . . . . . . . . . . .
11、. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 6 Z characters . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 7 Lexis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
12、 . . . . . . . . . . 24 8 Concrete syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 9 Characterisation rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 10 Annotated syntax . . . . . . . . .
13、 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 11 Prelude . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 12 Syntactic transformation rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
14、. . . . . . . . . . 44 13 Type inference rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 14 Semantic transformation rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66 15 Semantic relations . . . . . . . .
15、. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71 Annex A (normative) Mark-ups . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 Annex B (normative) Mathematical toolkit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
16、. . . 94 Annex C (normative) Organisation by concrete syntax production . . . . . . . . . . . . . . . . . . . . . . 111 Annex D (informative) Tutorial . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 158 Annex E (informative) Conventions for state-based description
17、s . . . . . . . . . . . . . . . . . . . . . . . . 173 Bibliography . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 175 Index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 176
18、 iii BSISO/IEC13568:2002Figures 1 Phases of the denition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 B.1 Parent relation between sections of the mathematical toolkit . . . . . . . . . . . . . . . . . . . . . . . 94 D.1 Concrete parse tree of birthday book
19、 example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 161 D.2 Tree of birthday book example after syntactic transformation . . . . . . . . . . . . . . . . . . . . . . 164 D.3 Annotated tree of axiomatic example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
20、165 D.4 Annotated tree of generic example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 168 D.5 Annotated tree of chained relation example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 172 Tables 1 Syntactic metalanguage . . . . . . . . . . . . . . . . .
21、 . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2 Parentheses in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 3 Propositional connectives in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 4 Quantiers in metala
22、nguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 5 Abbreviations in quantications in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 6 Conditional expression in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
23、 . . . . 5 7 Propositions about sets in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 8 Basic set operations in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 9 Powerset in metalanguage . . . . . . . . . . . . . . . . . . .
24、 . . . . . . . . . . . . . . . . . . . . . . . 7 10 Operations on natural numbers in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 11 Decorations of names in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 12 Tuples and Cartesian produc
25、ts in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 13 Function comprehensions in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 14 Relations in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
26、 . . 8 15 Proposition about relations in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 16 Functions in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 17 Application in metalanguage . . . . . . . . . . . . . . . . .
27、. . . . . . . . . . . . . . . . . . . . . . . 9 18 Sequences in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 19 Disjointness in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 20 Metavariables for phra
28、ses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 21 Metavariables for operator words . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 22 Environments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
29、. . . . . . . . . . 12 23 Metavariables for environments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 24 Variables over type universe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 25 Type relations . . . . . . . . . . . . . .
30、 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 26 Type sequents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 27 Semantic universe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31、 . . . 14 28 Variables over semantic universe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 29 Semantic relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 30 Semantic idioms . . . . . . . . . . . . . . . . . . . .
32、 . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 31 Operator precedences and associativities . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 iv BSISO/IEC13568:2002Foreword ISO (the International Organization for Standardization) and IEC (the International Electrotechn
33、ical Commission) form the specialized system for worldwide standardization. National bodies that are members of ISO or IEC participate in the development of International Standards through technical committees established by the respective organization to deal with particular fields of technical act
34、ivity. ISO and IEC technical committees collaborate in fields of mutual interest. Other international organizations, governmental and non-governmental, in liaison with ISO and IEC, also take part in the work. In the field of information technology, ISO and IEC have established a joint technical comm
35、ittee, ISO/IEC JTC 1. International Standards are drafted in accordance with the rules given in the ISO/IEC Directives, Part 3. The main task of the joint technical committee is to prepare International Standards. Draft International Standards adopted by the joint technical committee are circulated
36、to national bodies for voting. Publication as an International Standard requires approval by at least 75 % of the national bodies casting a vote. Attention is drawn to the possibility that some of the elements of this International Standard may be the subject of patent rights. ISO and IEC shall not
37、be held responsible for identifying any or all such patent rights. ISO/IEC 13568 was prepared by Joint Technical Committee ISO/IEC JTC 1, Information technology, Subcommittee SC 22, Programming languages, their environments and system software interfaces. Annexes A to C form a normative part of this
38、 International Standard. Annexes D and E are for information only. v BSISO/IEC13568:2002Introduction This International Standard species the syntax, type system and semantics of the Z notation, as used in formal specication. A specication of a system should aid understanding of that system, assistin
39、g development and maintenance of the system. Specications need express only abstract properties, unlike implementations such as detailed algorithms, physical circuits, etc. Specications may be loose, allowing renement to many dierent implementations. Such abstract and loose specications can be writt
40、en in Z notation. A specication written in Z notation models the specied system: it names the components of the system and expresses the constraints between those components. The meaning of a Z specication|its semantics|is dened as the set of interpretations (values for the named components) that ar
41、e consistent with the constraints. Z uses mathematical notation, hence specications written in Z are said to be formal: the meaning is captured by the form of the mathematics used, independent of the names chosen. This formal basis enables mathematical reasoning, and hence proofs that desired proper
42、ties are consequences of the specication. The soundness of inference rules used in such reasoning should be proven relative to the semantics of the Z notation. This International Standard establishes precise syntax and semantics for a system of notation for mathematics, providing a basis on which fu
43、rther mathematics can be formalized. Particular characteristics of Z include: its extensible toolkit of mathematical notation; its schema notation for specifying structures in the system and for structuring the specication itself; and its decidable type system, which allows some well-formedness chec
44、ks on a specication to be performed automatically. Examples of the kinds of systems that have been specied in Z include: safety critical systems, such as railway signalling, medical devices, and nuclear power systems; security systems, such as transaction processing systems, and communications; and
45、general systems, such as programming languages and oating point processors. Standard Z will also be appropriate for use in: formalizing the semantics of other notations, especially in standards documents. This is the rst ISO standard for the Z notation. Much has already been published about Z. Most
46、uses of the Z notation have been based on the examples in the book Specication Case Studies“ edited by Hayes 23. Early denitions of the notation were made by Sufrin 14 and by King et al 8. Spiveys doctoral thesis showed that the semantics of the notation could be dened in terms of sets of models in
47、ZF set theory 11. His book The Z Notation|A Reference Manual“ 1213 is the most complete denition of the notation, prior to this International Standard. Dierences between Z as dened here and as dened in 13 are discussed in 15. This International Standard addresses issues that have been resolved in di
48、erent ways by dierent users, and hence encourages interchange of specications between diverse tools. It also aims to be a complete formal denition of Z. vi BSISO/IEC13568:20021 BSISO/IEC13568:20024Metalanguages 3.2 capture cause a reference expression to refer to a dierent declaration from that inte
49、nded 3.3 carrier set set of all values in a type 3.4 constraint property that is either true or false 3.5 environment function from names to information used in type inference 3.6 interpretation function from global names of a section to values in the semantic universe 3.7 metalanguage language used for dening another language 3.8 metavariable name denoting an arbitrary phrase of a particular syntactic class 3.9 mode
