《ANSI-ISO-IEC-13568-2002.pdf》由会员分享，可在线阅读，更多相关《ANSI-ISO-IEC-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 Adopted by INCITS (InterNational Committee for Information Technology Standards) as an American National Standard.Adopted by INCITS (InterNational Committee for Information Technology Standards) as an American National Standard. Date of ANSI Approval: 12/20/2002 Published by American
3、 National Standards Institute, 25 West 43rd Street, New York, New York 10036 Copyright 2002 by Information Technology Industry Council (ITI). All rights reserved. These materials are subject to copyright claims of International Standardization Organization (ISO), International Electrotechnical Commi
4、ssion (IEC), American National Standards Institute (ANSI), and Information Technology Industry Council (ITI). Not for resale. No part of this publication may be reproduced in any form, including an electronic retrieval system, without the prior written permission of ITI. All requests pertaining to t
5、his standard should be submitted to ITI, 1250 Eye Street NW, Washington, DC 20005. Printed in the United States of America Copyright American National Standards Institute Provided by IHS under license with ANSI Licensee=IHS Employees/1111111001, User=OConnor, Maurice Not for Resale, 04/29/2007 12:31
6、:21 MDTNo reproduction or networking permitted without license from IHS -,-,- ISO/IEC 13568:2002(E) PDF 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 embed
7、ded are licensed to and installed on the computer performing the editing. In downloading this file, parties 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.
8、Details of the software products used to create this PDF file can be found in the General Info relative 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 probl
9、em relating to it is found, please inform the Central Secretariat at the address given below. ISO/IEC 2002 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 micr
10、ofilm, without permission in writing from either ISO at the address below or ISOs member body in the country of the requester. Permission is granted to reproduce mathematical definitions (i.e. syntactic definitions, syntactic transformations, type inference rules, semantic transformations and semant
11、ic relations) from this ISO standard, free of charge, on condition that the following statement is reproduced. “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
12、 copyrightiso.ch Web www.iso.ch Printed in Switzerland ii ISO/IEC 2002 All rights reserved Copyright American National Standards Institute Provided by IHS under license with ANSI Licensee=IHS Employees/1111111001, User=OConnor, Maurice Not for Resale, 04/29/2007 12:31:21 MDTNo reproduction or networ
13、king permitted without license from IHS -,-,- ISO/IEC 13568:2002(E) ContentsPage Foreword. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .v Introduction. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
14、. . . . . . . . .vi 1Scope. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1 2Normative references . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1 3 Terms and defi nitions. . . . . . . . . . .
15、. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1 4Metalanguages. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .3 5Conformance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
16、15 6Z characters . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .18 7Lexis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .24 8Concrete syntax. . . . . . . . . . . . . . . . . . . .
17、. . . . . . . . . . . . . . . . . . . . . . . . . . . . .30 9Characterisation rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .39 10Annotated syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .40 11Pre
18、lude . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .43 12Syntactic transformation rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .44 13Type inference rules . . . . . . . . . . . . . . . . . . . . . . .
19、 . . . . . . . . . . . . . . . . . . . . . . . .55 14Semantic transformation rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .66 15Semantic relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .71 Annex A (norma
20、tive)Mark-ups . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .79 Annex B (normative)Mathematical toolkit. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .94 Annex C (normative)Organisation by concrete syntax production . . . . . . . . . . . . . . . .
21、 . . . . . . 111 Annex D (informative)Tutorial . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 158 Annex E (informative)Conventions for state-based descriptions . . . . . . . . . . . . . . . . . . . . . . . . 173 Bibliography. . . . . . . . . . . . . . . . . . . .
22、 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 175 Index. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 176 c ?ISO/IEC 2002All rights reservediii Copyright American National Standards Institute Provided by IHS unde
23、r license with ANSI Licensee=IHS Employees/1111111001, User=OConnor, Maurice Not for Resale, 04/29/2007 12:31:21 MDTNo reproduction or networking permitted without license from IHS -,-,- ISO/IEC 13568:2002(E) Figures 1 Phases of the defi nition. . . . . . . . . . . . . . . . . . . . . . . . . . . .
24、. . . . . . . . . . . . . . .16 B.1Parent relation between sections of the mathematical toolkit . . . . . . . . . . . . . . . . . . . . . . .94 D.1Concrete parse tree of birthday book example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 161 D.2Tree of birthday book example after syn
25、tactic transformation . . . . . . . . . . . . . . . . . . . . . . 164 D.3Annotated tree of axiomatic example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 165 D.4Annotated tree of generic example. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 168 D
26、.5Annotated tree of chained relation example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 172 Tables 1Syntactic metalanguage. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .3 2Parentheses in metalanguage. . . . . . . . . . . . . . . . . . . . .
27、. . . . . . . . . . . . . . . . . . .4 3Propositional connectives in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .5 4 Quantifi ers in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .5 5 Abbreviations in quantifi cations i
28、n metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . .5 6Conditional expression in metalanguage. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .5 7Propositions about sets in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6 8Basic s
29、et operations in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6 9Powerset in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .7 10Operations on natural numbers in metalanguage. . . . . . . . . . . . . . . . . . . .
30、 . . . . . . . . .7 11Decorations of names in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .7 12Tuples and Cartesian products in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8 13Function comprehensions in metalanguage . . . . . . . . . .
31、 . . . . . . . . . . . . . . . . . . . . . . .8 14Relations in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8 15Proposition about relations in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8 16Functions in metalanguage
32、. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .9 17Application in metalanguage. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .9 18Sequences in metalanguage. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33、. .9 19Disjointness in metalanguage. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .9 20Metavariables for phrases. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .10 21Metavariables for operator words . . . . . . . . . . . . . . . . . .
34、. . . . . . . . . . . . . . . . . . . .11 22Environments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12 23Metavariables for environments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12 24Variables over type universe
35、 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12 25Type relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12 26Type sequents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
36、. . . . . . . .13 27Semantic universe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .14 28Variables over semantic universe. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .14 29Semantic relations. . . . . . . . . . . . . . . . .
37、. . . . . . . . . . . . . . . . . . . . . . . . . . . . .14 30Semantic idioms. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .15 31Operator precedences and associativities . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .37 ivc ?ISO/IEC 2
38、002All rights reserved Copyright American National Standards Institute Provided by IHS under license with ANSI Licensee=IHS Employees/1111111001, User=OConnor, Maurice Not for Resale, 04/29/2007 12:31:21 MDTNo reproduction or networking permitted without license from IHS -,-,- ISO/IEC 13568:2002(E)
39、Foreword c ?ISO/IEC 2002All rights reservedv ISO (the International Organization for Standardization) 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 In
40、ternational Standards through technical committees established by the respective organization 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 liai
41、son with ISO and IEC, also take part in the work. In the field of information technology, ISO 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 tech
42、nical committee is to prepare International Standards. Draft International Standards adopted 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
43、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 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 technolog
44、y, Subcommittee SC 22, Programming languages, their environments and system software interfaces. Annexes A to C form a normative part of this International Standard. Annexes D and E are for information only. Copyright American National Standards Institute Provided by IHS under license with ANSI Lice
45、nsee=IHS Employees/1111111001, User=OConnor, Maurice Not for Resale, 04/29/2007 12:31:21 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 use
46、d in formal specifi cation. A specifi cation of a system should aid understanding of that 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 ma
47、y be loose, allowing refi nement to many diff erent implementations. Such abstract and 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
48、. The meaning of a Z specifi cationits semanticsis defi ned as the set of interpretations (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 mat
49、hematics used, independent of the names chosen. This formal basis enables mathematical 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 se