《ISO-13568-2002.pdf》由会员分享，可在线阅读，更多相关《ISO-13568-2002.pdf（196页珍藏版）》请在三一文库上搜索。
1、 Reference number ISO/IEC 13568:2002(E) ISO/IEC 2002 INTERNATIONAL STANDARD ISO/IEC 13568 First edition 2002-07-01 Information technology Z formal specification notation Syntax, type system and semantics Technologies de linformation Notation Z pour la spcification formelle Syntaxe, systme de caractr
2、es et smantique Copyright International Organization for Standardization Provided by IHS under license with ISO Licensee=IHS Employees/1111111001, User=Wing, Bernie Not for Resale, 04/03/2007 01:10:19 MDTNo reproduction or networking permitted without license from IHS -,-,- ISO/IEC 13568:2002(E) PDF
3、 disclaimer This PDF file may contain embedded typefaces. In accordance with Adobes licensing policy, this file may be printed or viewed but shall not be edited unless the typefaces which are embedded are licensed to and installed on the computer performing the editing. In downloading this file, par
4、ties accept therein the responsibility of not infringing Adobes licensing policy. The ISO Central Secretariat accepts no liability in this area. Adobe is a trademark of Adobe Systems Incorporated. Details of the software products used to create this PDF file can be found in the General Info relative
5、 to the file; the PDF-creation parameters were optimized for printing. Every care has been taken to ensure that the file is suitable for use by ISO member bodies. In the unlikely event that a problem relating to it is found, please inform the Central Secretariat at the address given below. ISO/IEC 2
6、002 All rights reserved. Unless otherwise specified, no part of this publication may be reproduced or utilized in any form or by any means, electronic or mechanical, including photocopying and microfilm, without permission in writing from either ISO at the address below or ISOs member body in the co
7、untry of the requester. Permission is granted to reproduce mathematical definitions (i.e. syntactic definitions, syntactic transformations, type inference rules, semantic transformations and semantic relations) from this ISO standard, free of charge, on condition that the following statement is repr
8、oduced. “Mathematical definitions from ISO/IEC 13568:2002 (Z standard) are copyright ISO.” ISO copyright office Case postale 56 CH-1211 Geneva 20 Tel. + 41 22 749 01 11 Fax + 41 22 749 09 47 E-mail copyrightiso.ch Web www.iso.ch Printed in Switzerland ii ISO/IEC 2002 All rights reserved Copyright In
9、ternational Organization for Standardization Provided by IHS under license with ISO Licensee=IHS Employees/1111111001, User=Wing, Bernie Not for Resale, 04/03/2007 01:10:19 MDTNo reproduction or networking permitted without license from IHS -,-,- ISO/IEC 13568:2002(E) ContentsPage Foreword. . . . .
10、. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .v Introduction. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .vi 1Scope. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
11、 . . . . . . . . . . . . . . . . . .1 2Normative references . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1 3 Terms and defi nitions. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1 4Metalanguages. . . . . . .
12、. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .3 5Conformance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .15 6Z characters . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
13、. . . . . . . . . . .18 7Lexis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .24 8Concrete syntax. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .30 9Characterisation rules . . . . . . . .
14、 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .39 10Annotated syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .40 11Prelude . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
15、. . . . . . .43 12Syntactic transformation rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .44 13Type inference rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .55 14Semantic transformation rules . . . . . . . .
16、. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .66 15Semantic relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .71 Annex A (normative)Mark-ups . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .79 A
17、nnex B (normative)Mathematical toolkit. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .94 Annex C (normative)Organisation by concrete syntax production . . . . . . . . . . . . . . . . . . . . . . 111 Annex D (informative)Tutorial . . . . . . . . . . . . . . . . . . . . . . . . . .
18、. . . . . . . . . . . . . . . . 158 Annex E (informative)Conventions for state-based descriptions . . . . . . . . . . . . . . . . . . . . . . . . 173 Bibliography. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 175 Index. . . . . . . . . . . .
19、 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 176 c ?ISO/IEC 2002All rights reservediii Copyright International Organization for Standardization Provided by IHS under license with ISO Licensee=IHS Employees/1111111001, User=Wing, Bernie Not for Resale, 04
20、/03/2007 01:10:19 MDTNo reproduction or networking permitted without license from IHS -,-,- ISO/IEC 13568:2002(E) Figures 1 Phases of the defi nition. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .16 B.1Parent relation between sections of the mathematical toolkit
21、 . . . . . . . . . . . . . . . . . . . . . . .94 D.1Concrete parse tree of birthday book example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 161 D.2Tree of birthday book example after syntactic transformation . . . . . . . . . . . . . . . . . . . . . . 164 D.3Annotated tree of axio
22、matic example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 165 D.4Annotated tree of generic example. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 168 D.5Annotated tree of chained relation example . . . . . . . . . . . . . . . . . . . . . . . . .
23、. . . . . . . 172 Tables 1Syntactic metalanguage. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .3 2Parentheses in metalanguage. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .4 3Propositional connectives in metalanguage . . . . . . .
24、 . . . . . . . . . . . . . . . . . . . . . . . . . .5 4 Quantifi ers in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .5 5 Abbreviations in quantifi cations in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . .5 6Conditional expressi
25、on in metalanguage. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .5 7Propositions about sets in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6 8Basic set operations in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
26、 . . .6 9Powerset in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .7 10Operations on natural numbers in metalanguage. . . . . . . . . . . . . . . . . . . . . . . . . . . . .7 11Decorations of names in metalanguage . . . . . . . . . . . . . . . . . .
27、. . . . . . . . . . . . . . . . .7 12Tuples and Cartesian products in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8 13Function comprehensions in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8 14Relations in metalanguage . . . . . . . . . .
28、 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8 15Proposition about relations in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8 16Functions in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .9 17Applicat
29、ion in metalanguage. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .9 18Sequences in metalanguage. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .9 19Disjointness in metalanguage. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30、. . . . . . . . . .9 20Metavariables for phrases. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .10 21Metavariables for operator words . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .11 22Environments . . . . . . . . . . . . . . . . . . .
31、. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12 23Metavariables for environments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12 24Variables over type universe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12 25Type rel
32、ations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12 26Type sequents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .13 27Semantic universe . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33、 . . . . . . . . . . . . . . . . . .14 28Variables over semantic universe. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .14 29Semantic relations. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .14 30Semantic idioms. . . . . . . . .
34、. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .15 31Operator precedences and associativities . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .37 ivc ?ISO/IEC 2002All rights reserved Copyright International Organization for Standardization Provided by IHS
35、 under license with ISO Licensee=IHS Employees/1111111001, User=Wing, Bernie Not for Resale, 04/03/2007 01:10:19 MDTNo reproduction or networking permitted without license from IHS -,-,- ISO/IEC 13568:2002(E) Foreword c ?ISO/IEC 2002All rights reservedv ISO (the International Organization for Standa
36、rdization) and IEC (the International Electrotechnical 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 organizati
37、on to deal with particular fields of technical activity. 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, I
38、SO and IEC have established a joint technical committee, 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 adopte
39、d by the joint technical committee are circulated 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 th
40、e subject of patent rights. ISO and IEC shall not 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 interf
41、aces. Annexes A to C form a normative part of this International Standard. Annexes D and E are for information only. Copyright International Organization for Standardization Provided by IHS under license with ISO Licensee=IHS Employees/1111111001, User=Wing, Bernie Not for Resale, 04/03/2007 01:10:1
42、9 MDTNo reproduction or networking permitted without license from IHS -,-,- ISO/IEC 13568:2002(E) Introduction This International Standard specifi es the syntax, type system and semantics of the Z notation, as used in formal specifi cation. A specifi cation of a system should aid understanding of th
43、at system, assisting development and maintenance of the system. Specifi cations need express only abstract properties, unlike implementations such as detailed algorithms, physical circuits, etc. Specifi cations may be loose, allowing refi nement to many diff erent implementations. Such abstract and
44、loose specifi cations can be written in Z notation. A specifi cation written in Z notation models the specifi ed system: it names the components of the system and expresses the constraints between those components. The meaning of a Z specifi cationits semanticsis defi ned as the set of interpretatio
45、ns (values for the named components) that are consistent with the constraints. Z uses mathematical notation, hence specifi cations 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
46、reasoning, and hence proofs that desired properties are consequences of the specifi cation.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 notati
47、on for mathematics, providing a basis on which further 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 specifi cation itself; and its decidable
48、 type system, which allows some well-formedness checks on a specifi cation to be performed automatically. Examples of the kinds of systems that have been specifi ed in Z include: safety critical systems, such as railway signalling, medical devices, and nuclear power systems; security systems, such a
49、s transaction processing systems, and communications; and general systems, such as programming languages and fl 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 fi rst ISO standard for the Z notation. Much has already be