ANSI INCITS ISO IEC 13568-2002 Information technology - Z formal specification notation - Syntax type system and semantics.pdf

1、 Reference numberISO/IEC 13568:2002(E)ISO/IEC 2002INTERNATIONAL STANDARD ISO/IEC13568First edition2002-07-01Information technology Z formal specification notation Syntax, type system and semantics Technologies de linformation Notation Z pour la spcification formelle Syntaxe, systme de caractres et s

2、mantique Adopted by INCITS (InterNational Committee for Information Technology Standards) as an American National Standard.Date of ANSI Approval: 12/20/2002Published by American National Standards Institute,25 West 43rd Street, New York, New York 10036Copyright 2002 by Information Technology Industr

3、y Council (ITI).All rights reserved.These materials are subject to copyright claims of International Standardization Organization (ISO), InternationalElectrotechnical Commission (IEC), American National Standards Institute (ANSI), and Information Technology Industry Council(ITI). Not for resale. No

4、part of this publication may be reproduced in any form, including an electronic retrieval system, withoutthe prior written permission of ITI. All requests pertaining to this standard should be submitted to ITI, 1250 Eye Street NW,Washington, DC 20005.Printed in the United States of AmericaISO/IEC 13

5、568: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 embedded are licensed to and installed on the computer performing the editing. In downloading

6、 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. Details of the software products used to create this PDF file can be found in the Genera

7、l 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 problem relating to it is found, please inform the Central Secretariat at the address given b

8、elow. 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 microfilm, without permission in writing from either ISO at the address below or ISOs member

9、 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 semantic relations) from this ISO standard, free of charge, on condition that the following st

10、atement 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 copyrightiso.ch Web www.iso.ch Printed in Switzerland ii ISO/IEC 2002 All rights reserv

11、ed ISO/IEC 13568:2002(E)Contents PageForeword . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . vIntroduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . vi1 Scope . . . . . . .

12、. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 Normative references . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 Terms and de nitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

13、. . . . . . . . . . . . . . . 14 Metalanguages . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Conformance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 156 Z characters . . . . . . . . . .

14、 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 187 Lexis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 248 Concrete syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

15、 . . . . . . . . . . . . 309 Characterisation rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3910 Annotated syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4011 Prelude . . . . . . . . . . . . .

16、 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4312 Syntactic transformation rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4413 Type inference rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

17、 . . . . . . . . . . 5514 Semantic transformation rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6615 Semantic relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71Annex A (normative) Mark-ups . . . . . .

18、 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79Annex B (normative) Mathematical toolkit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94Annex C (normative) Organisation by concrete syntax production . . . . . . . . . . . . . . . . . . . . . . 111Annex

19、D (informative) Tutorial . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 158Annex E (informative) Conventions for state-based descriptions . . . . . . . . . . . . . . . . . . . . . . . . 173Bibliography . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

20、 . . . . . . . . . . . . . . . . . . . . . . 175Index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 176c ISO/IEC 2002|All rights reserved iiiISO/IEC 13568:2002(E)Figures1 Phases of the de nition . . . . . . . . . . . . . . . . . . .

21、 . . . . . . . . . . . . . . . . . . . . . . . . 16B.1 Parent relation between sections of the mathematical toolkit . . . . . . . . . . . . . . . . . . . . . . . 94D.1 Concrete parse tree of birthday book example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 161D.2 Tree of birthday b

22、ook example after syntactic transformation . . . . . . . . . . . . . . . . . . . . . . 164D.3 Annotated tree of axiomatic example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 165D.4 Annotated tree of generic example . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

23、 . . . . . . . . 168D.5 Annotated tree of chained relation example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 172Tables1 Syntactic metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Parentheses in metalanguage . . . . . . . . .

24、. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 Propositional connectives in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 Quanti ers in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 Abbreviation

25、s in quanti cations in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 Conditional expression in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 Propositions about sets in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . .

26、 . . . . . . . 68 Basic set operations in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69 Powerset in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 710 Operations on natural numbers in metalanguage . . . . . .

27、 . . . . . . . . . . . . . . . . . . . . . . . 711 Decorations of names in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 712 Tuples and Cartesian products in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 813 Function comprehensions in m

28、etalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 814 Relations in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 815 Proposition about relations in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

29、. . 816 Functions in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 917 Application in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 918 Sequences in metalanguage . . . . . . . . . . . . . . . . . . . .

30、. . . . . . . . . . . . . . . . . . . . . 919 Disjointness in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 920 Metavariables for phrases . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1021 Metavariables for operator

31、 words . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1122 Environments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1223 Metavariables for environments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

32、 . . . . . . 1224 Variables over type universe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1225 Type relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1226 Type sequents . . . . . . . . . . . . . . . . .

33、. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1327 Semantic universe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1428 Variables over semantic universe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1429

34、Semantic relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1430 Semantic idioms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1531 Operator precedences and associativities . . . . . . . . . . . . . .

35、. . . . . . . . . . . . . . . . . . . . 37iv c ISO/IEC 2002|All rights reservedISO/IEC 13568:2002(E)Forewordc ISO/IEC 2002|All rights reserved vISO (the International Organization for Standardization) and IEC (the International Electrotechnical Commission) form the specialized system for worldwide s

36、tandardization. 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 activity. ISO and IEC technical committees collaborate in field

37、s 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 committee, ISO/IEC JTC 1. International Standards are drafted in

38、 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 to national bodies for voting. Publication as an Internation

39、al 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 be held responsible for identifying any or all such patent r

40、ights. 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 International Standard. Annexes D and E are for information

41、 only. ISO/IEC 13568:2002(E)IntroductionThis International Standard speci es the syntax, type system and semantics of the Z notation, as used in formalspeci cation.A speci cation of a system should aid understanding of that system, assisting development and maintenance of thesystem. Speci cations ne

42、ed express only abstract properties, unlike implementations such as detailed algorithms,physical circuits, etc. Speci cations may be loose, allowing re nement to many di erent implementations. Suchabstract and loose speci cations can be written in Z notation.A speci cation written in Z notation mode

43、ls the speci ed system: it names the components of the system andexpresses the constraints between those components. The meaning of a Z speci cation|its semantics|is de nedas the set of interpretations (values for the named components) that are consistent with the constraints.Z uses mathematical not

44、ation, hence speci cations written in Z are said to be formal: the meaning is capturedby the form of the mathematics used, independent of the names chosen. This formal basis enables mathematicalreasoning, and hence proofs that desired properties are consequences of the speci cation. The soundness of

45、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 further mathematics can be formalized.Particular characteristic

46、s of Z include:its extensible toolkit of mathematical notation;its schema notation for specifying structures in the system and for structuring the speci cation itself; andits decidable type system, which allows some well-formedness checks on a speci cation to be performedautomatically.Examples of th

47、e kinds of systems that have been speci ed 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; andgeneral systems, such as programming languages and oating point pro

48、cessors.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 uses of theZ notation have been based on the examples in the book Spec

49、i cation Case Studies“ edited by Hayes 23.Early de nitions of the notation were made by Sufrin 14 and by King et al 8. Spiveys doctoral thesis showedthat the semantics of the notation could be de ned in terms of sets of models in ZF set theory 11. His bookThe Z Notation|A Reference Manual“ 1213 is the most complete de nition of the notation, prior to thisInternational Standard. Di erences between Z as de ned here and as de ned in 13 are discussed in 15. ThisInternational Standard addresses issues that have been resolved in di erent ways by di ere