1、 Reference numberISO/IEC 13568:2002(E)ISO/IEC 2002 INTERNATIONAL 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 sm
2、antique 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 embedded are licensed to and installed on the computer performing the editing.
3、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.Details of the software products used to create this PDF file can be found in
4、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 problem relating to it is found,please inform the Central Secretariat at the address g
5、iven 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 microfilm,without permission in writing from either ISO at the address below or ISOs member
6、 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 statement i
7、s 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 reserved ISO/IEC 13568
8、:2002(E)ContentsPageForeword.vIntroduction.vi1Scope.12Normative references.13Terms and definitions.14Metalanguages.35Conformance.156Z characters.187Lexis.248Concrete syntax.309Characterisation rules.3910Annotated syntax.4011Prelude.4312Syntactic transformation rules.4413Type inference rules.5514Sema
9、ntic transformation rules.6615Semantic relations.71Annex A(normative)Mark-ups.79Annex B(normative)Mathematical toolkit.94Annex C(normative)Organisation by concrete syntax production.111Annex D(informative)Tutorial.158Annex E(informative)Conventions for state-based descriptions.173Bibliography.175Ind
10、ex.176c?ISO/IEC 2002All rights reservediiiISO/IEC 13568:2002(E)Figures1Phases of the definition.16B.1Parent relation between sections of the mathematical toolkit.94D.1Concrete parse tree of birthday book example.161D.2Tree of birthday book example after syntactic transformation.164D.3Annotated tree
11、of axiomatic example.165D.4Annotated tree of generic example.168D.5Annotated tree of chained relation example.172Tables1Syntactic metalanguage.32Parentheses in metalanguage.43Propositional connectives in metalanguage.54Quantifiers in metalanguage.55Abbreviations in quantifications in metalanguage.56
12、Conditional expression in metalanguage.57Propositions about sets in metalanguage.68Basic set operations in metalanguage.69Powerset in metalanguage.710Operations on natural numbers in metalanguage.711Decorations of names in metalanguage.712Tuples and Cartesian products in metalanguage.813Function com
13、prehensions in metalanguage.814Relations in metalanguage.815Proposition about relations in metalanguage.816Functions in metalanguage.917Application in metalanguage.918Sequences in metalanguage.919Disjointness in metalanguage.920Metavariables for phrases.1021Metavariables for operator words.1122Envir
14、onments.1223Metavariables for environments.1224Variables over type universe.1225Type relations.1226Type sequents.1327Semantic universe.1428Variables over semantic universe.1429Semantic relations.1430Semantic idioms.1531Operator precedences and associativities.37ivc?ISO/IEC 2002All rights reservedISO
15、/IEC 13568:2002(E)Forewordc?ISO/IEC 2002All rights reservedvISO(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 develop
16、ment 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 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 committee,ISO/IEC JTC 1.International Standards are drafted