CAN CSA-ISO IEC 13568-2004 Information technology - Z formal specification notation - Syntax type system and semantics (Incorporates Corrigendum September 2008).pdf

1、 Reference numberISO/IEC 13568:2002(E)ISO/IEC 2002Information technology Z formal specification notation Syntax, type system and semantics Technologies de linformation Notation Z pour la spcification formelle Syntaxe, systme de caractres et smantique National Standard of CanadaCAN/CSA-ISO/IEC 13568:

2、04(ISO/IEC 13568:2002)International Standard ISO/IEC 13568:2002 (first edition, 2002-07-01) has been adopted without modification(IDT) as CSA Standard CAN/CSA-ISO/IEC 13568:04, which has been approved as a National Standard of Canadaby the Standards Council of Canada.ISBN 1-55397-323-2 January 2004T

3、he Canadian Standards Association (CSA), The Standards Council of Canada is theunder whose auspices this National Standard has been coordinating body of the National Standards system, produced, was chartered in 1919 and accredited by a federation of independent, autonomousthe Standards Council of Ca

4、nada to the National organizations working towards the furtherStandards system in 1973. It is a not-for-profit, development and improvement of voluntarynonstatutory, voluntary membership association standardization in the national interest.engaged in standards development and certification The princ

5、ipal objects of the Council are to foster activities. and promote voluntary standardization as a means CSA standards reflect a national consensus of of advancing the national economy, benefiting theproducers and users including manufacturers, health, safety, and welfare of the public, assisting cons

6、umers, retailers, unions and professional and protecting the consumer, facilitating domestic organizations, and governmental agencies. The and international trade, and furthering internationalstandards are used widely by industry and commerce cooperation in the field of standards.and often adopted b

7、y municipal, provincial, and A National Standard of Canada is a standard whichfederal governments in their regulations, particularly in has been approved by the Standards Council ofthe fields of health, safety, building and construction, Canada and one which reflects a reasonableand the environment.

8、 agreement among the views of a number of capableIndividuals, companies, and associations across individuals whose collective interests provide to theCanada indicate their support for CSAs standards greatest practicable extent a balance ofdevelopment by volunteering their time and skills to represen

9、tation of producers, users, consumers, andCSA Committee work and supporting the Associations others with relevant interests, as may be appropriateobjectives through sustaining memberships. The more to the subject in hand. It normally is a standardthan 7000 committee volunteers and the 2000 which is

10、capable of making a significant and timelysustaining memberships together form CSAs total contribution to the national interest.membership from which its Directors are chosen. Approval of a standard as a National Standard ofSustaining memberships represent a major source of Canada indicates that a s

11、tandard conforms to theincome for CSAs standards development activities. criteria and procedures established by the StandardsThe Association offers certification and testing Council of Canada. Approval does not refer to theservices in support of and as an extension to its technical content of the st

12、andard; this remains thestandards development activities. To ensure the continuing responsibility of the accreditedintegrity of its certification process, the Association standards-development organization.regularly and continually audits and inspects products Those who have a need to apply standard

13、s arethat bear the CSA Mark. encouraged to use National Standards of CanadaIn addition to its head office and laboratory complex whenever practicable. These standards are subject in Toronto, CSA has regional branch offices in major to periodic review; therefore, users are cautioned centres across Ca

14、nada and inspection and testing to obtain the latest edition from the organizationagencies in eight countries. Since 1919, the preparing the standard.Association has developed the necessary expertise to The responsibility for approving National Standards meet its corporate mission: CSA is an indepen

15、dent of Canada rests with theservice organization whose mission is to provide an Standards Council of Canadaopen and effective forum for activities facilitating the 270 Albert Street, Suite 200exchange of goods and services through the use of Ottawa, Ontario, K1P 6N7standards, certification and rela

16、ted services to meet Canadanational and international needs.For further information on CSA services, write toCanadian Standards Association5060 Spectrum Way, Suite 100Mississauga, Ontario, L4W 5N6CanadaAlthough the intended primary application of this Standard is stated in its Scope, it is important

17、to note that it remains the responsibility of the users to judge its suitability for their particular purpose.Registered trade-mark of Canadian Standards AssociationCAN/CSA-ISO/IEC 13568:04 type system and semanticsInformation technology Z formal specification notation Syntax,January 2004 Canadian S

18、tandards Association CSA/1CAN/CSA-ISO/IEC 13568:04Information technology Z formalspecification notation Syntax,type system and semanticsCSA PrefaceStandards development within the Information Technology sector is harmonized with internationalstandards development. Through the CSA Technical Committee

19、 on Information Technology (TCIT),Canadians serve as the Canadian Advisory Committee (CAC) on ISO/IEC Joint Technical Committee 1 onInformation Technology (ISO/IEC JTC1) for the Standards Council of Canada (SCC), the ISO memberbody for Canada and sponsor of the Canadian National Committee of the IEC

20、. Also, as a member of theInternational Telecommunication Union (ITU), Canada participates in the International Telegraph andTelephone Consultative Committee (ITU-T).This International Standard was reviewed by the CSA TCIT under the jurisdiction of the StrategicSteering Committee on Information Tech

21、nology and deemed acceptable for use in Canada. (Acommittee membership list is available on request from the CSA Project Manager.) From time to time,ISO/IEC may publish addenda, corrigenda, etc. The CSA TCIT will review these documents for approvaland publication. For a listing, refer to the CSA Inf

22、ormation Products catalogue or CSA Info Update orcontact a CSA Sales representative. This Standard has been formally approved, without modification, bythe Technical Committee and has been approved as a National Standard of Canada by the StandardsCouncil of Canada.January 2004 Canadian Standards Asso

23、ciation 2004All rights reserved. No part of this publication may be reproduced in any form whatsoever without the prior permission ofthe publisher. ISO/IEC material is reprinted with permission. Where the words “this International Standard” appear in thetext, they should be interpreted as “this Nati

24、onal Standard of Canada”. Inquiries regarding this National Standard of Canada should be addressed to Canadian Standards Association 5060 Spectrum Way, Suite 100, Mississauga, Ontario, Canada L4W 5N6 1-800-463-6727 416-747-4044www.csa.caICS 35.060 Ref. No. ISO/IEC 13568:2002/Cor.1:2007(E) ISO/IEC 20

25、07 All rights reserved INTERNATIONAL STANDARD ISO/IEC 13568:2002 TECHNICAL CORRIGENDUM 1 Published 2007-07-15 INTERNATIONAL ORGANIZATION FOR STANDARDIZATION ORGANISATION INTERNATIONALE DE NORMALISATIONINTERNATIONAL ELECTROTECHNICAL COMMISSION COMMISSION LECTROTECHNIQUE INTERNATIONALEInformation tech

26、nology Z formal specification notation Syntax, type system and semantics TECHNICAL CORRIGENDUM 1 Technologies de linformation Notation Z pour la spcification formelle Syntaxe, systme de caractres et smantique RECTIFICATIF TECHNIQUE 1 Technical Corrigendum 1 to ISO/IEC 13568:2002 was prepared by Join

27、t Technical Committee ISO/IEC JTC 1, Information technology, Subcommittee SC 22, Programming languages, their environments and system software interfaces. International Organization for Standardization (ISO), 2007. All rights reserved. International Electrotechnical Commission (IEC), 2007. All right

28、s reserved. NOT FOR RESALE. Technical Corrigendum 1:2008 toNational Standard of CanadaCAN/CSA-ISO/IEC 13568:04Technical Corrigendum 1:2007 to International Standard ISO/IEC 13568:2002 has been adopted withoutmodification (IDT) as Technical Corrigendum 1:2008 to CSA Standard CAN/CSA-ISO/IEC 13568:04.

29、 ThisTechnical Corrigendum was reviewed by the CSA Technical Committee on Information Technology (TCIT)under the jurisdiction of the Strategic Steering Committee on Information Technology and deemed acceptablefor use in Canada.September 2008ISO/IEC 13568:2002/Cor.1:2007Defect 13568/001: Use of UCSPa

30、ge 18, in 6.1At the end of the first paragraph, add the following sentences.“Reference is also made to characters General Category and to decimal digits Decimal DigitValue, as defined for the characters by Unicode18. The characters are assumed to be inNormalization Form C19.”Page 19, in 6.2In line 8

31、, replace “other UCS chars with Number property, but Number, Decimal Digit” by“any other UCS characters with General Category N* except Nd”.In line 11, replace “Number, Decimal Digit property” by “General Category Nd”.In line 14, replace “any characters of the mathematical toolkit with letter proper

32、ty” by “char-acters of the mathematical toolkit with General Category L*”.In line 15, replace “letter property” by “General Category L*”.In lines 34-35, replace “any characters of the mathematical toolkit with neither letter or numberproperty” by “characters of the mathematical toolkit with General

33、Category neither L* nor N*”.In lines 36-37, replace “neither letter or number property” by “General Category S*, P* orM*”.Page 20, in 6.3In line 4, replace “property” by “General Category”.Page 20, in 6.4.2In line 5, replace “UCS defines a corresponding decimal digit value” by “Unicode defines acorr

34、esponding Decimal Digit Value”.Page 21, in 6.4.3.3In line 1, replace “UCS letter property” by “General Category L*”.Page 21, in 6.4.4.1In line 2, replace “0000 02B9 MODIFIER LETTER PRIME” by “0000 2032 PRIME”.Page 21, in 6.4.4.3In line 10, replace “0000 300A LEFT DOUBLE ANGLE BRACKET” by “0000 27EA

35、MATH-EMATICAL LEFT DOUBLE ANGLE BRACKET”.In line 11, replace “0000 300B RIGHT DOUBLE ANGLE BRACKET” by “0000 27EB MATH-EMATICAL RIGHT DOUBLE ANGLE BRACKET”.1ISO/IEC 13568:2002/Cor.1:2007(E) Technical Corrigendum 1:2008 toCAN/CSA-ISO/IEC 13568:04Page 22, in 6.4.4.4In line 6, replace “| 0000 2028 LINE

36、 SEPARATOR” by “ 0000 2500 BOX DRAWINGSLIGHT HORIZONTAL”.In line 10, replace “(new line) 0000 2029 PARAGRAPH SEPARATOR” by “rightanglesw 0000 2514 BOXDRAWINGS LIGHT UP AND RIGHT”.Page 22, in 6.4.4.5In line 2, replace “0000 000A LINE FEED” by “0000 2028 LINE SEPARATOR”.At the end, add the following.“

37、Newlines represented in accordance with 20 shall all be treated as NLCHAR.NOTE 1 This ensures the conventional interpretation of LINE FEED (LF), LINE TABULA-TION (VT), FORM FEED (FF), CARRIAGE RETURN (CR) and NEXT LINE (NEL).All Unicode characters with General Category Zs shall be treated as SPACE.N

38、OTE 2 This includes the characters SPACE, EN SPACE, EM SPACE, THREE-PER-EMSPACE, FOUR-PER-EM SPACE, SIX-PER-EM SPACE, PUNCTUATION SPACE, THINSPACE, HAIR SPACE, MEDIUM MATHEMATICAL SPACE. It excludes CHARACTERTABULATION.”Page 23, in 6.4.6.1In line 11, replace “0000 005C REVERSE SOLIDUS” by “0000 2216

39、 SET MINUS”.Page 24, in 6.4.6.5In line 3, replace “0000 3008 LEFT ANGLE BRACKET” by “0000 27E8 MATHEMATICALLEFT ANGLE BRACKET”.In line 4, replace “0000 3009 RIGHT ANGLE BRACKET” by “0000 27E9 MATHEMATICALRIGHT ANGLE BRACKET”.Page 83, in A.2.4.3In line 5, replace “U+300A” by “U+27EA”.In line 6, repla

40、ce “U+300B” by “U+27EB”.Page 86, in A.2.5.1In line 11, replace “U+005C” by “U+2216”.Page 87, in A.2.5.5In line 6, replace “3008” by “27E8”.In line 7, replace “3009” by “27E9”.Page 175, in BibliographyIn line 9, delete “1)”, and delete the corresponding footnote (“To be published”).Add the following

41、references.“18 The Unicode Consortium, The Unicode Standard, Version 5.0.0, defined by: The UnicodeStandard, Version 5.0 (Boston, MA, Addison-Wesley, 2007. ISBN 0-321-48091-0)”“19 The Unicode Consortium, Unicode Standard Annex #15: Unicode Normalization Forms(http:/www.unicode.org/reports/tr15/)”“20

42、 The Unicode Consortium, Unicode Standard Annex #14: Line Breaking Properties(http:/www.unicode.org/reports/tr14/)”2ISO/IEC 13568:2002/Cor.1:2007(E) Technical Corrigendum 1:2008 toCAN/CSA-ISO/IEC 13568:04Defect 13568/002: LATEX zed environmentPage 88, in A.2.7.1Replace this clause by “Each formal Z

43、paragraph appears between a pair of beginxxx andendxxx LATEX environment commands. Text not appearing between such commands isinformal narrative.”Page 89Insert new clause: “A.2.7.6 Other paragraph mark-upOther unboxed formal paragraphs (those rendered without an outline) shall be enclosed in aLATEX

44、zed environment.beginzed.endzedThe mark-up beginzed shall be converted to a ZEDCHAR character. The mark-up endzedshall be converted to an ENDCHAR character.”Defect 13568/003: LATEX theorem environmentPage 89Insert the following at beginning of the new A.2.7.6.“Conjecture paragraphs shall be enclosed

45、 in a LATEX theorem environment, which takes a singleargument containing a name for the conjecture.begintheoremname.endtheoremThe mark-up begintheoremnameshall be converted to a ZEDCHAR character. The mark-upendtheorem shall be converted to an ENDCHAR character.”Page 184, in IndexAdd the following e

46、ntries.“LATEX mark-up environment,axdef, 88gendef, 88schema, 88theorem, 89zed, 89”3ISO/IEC 13568:2002/Cor.1:2007(E) Technical Corrigendum 1:2008 toCAN/CSA-ISO/IEC 13568:04Defect 13568/004: Semantic equation for schema universal quan-tification expressionPage 76, in 15.2.5.13Replace this semantic rel

47、ation by e (e oo Pi : ; .; in : n) oo P E = M : Model t : T M | t : e EM i,.,in(t t) e E(M t) tIn the narrative that follows, insert “appropriately restricted” before “union”.Repeat the same changes on page 133, in C.6.2.3.Defect 13568/005: Range of operator precedencesPage 36, in 8.3Add “NOTE 5 The

48、 range of an operators Prec NUMERAL is not constrained.”Defect 13568/006: Lexis of punctuation charactersPage 19, in 6.2In line 6, after “LETTER” insert “| PUNCT”.After line 25, before the definition of SPECIAL, insert the following new rule.PUNCT = , | ; | : | . ;In line 32, in the SYMBOL rule, del

49、ete “: | ; | , | . | ”.In line 37, in the SYMBOL rule, replace “SPECIAL” with “PUNCT or SPECIAL”.Page 20, in 6.3In lines 5 and 6, replace “SPECIAL” with “PUNCT or SPECIAL”.Page 21, before 6.4.4Insert “6.4.4 Punctuation charactersMath Code position Character name, 0000 002C COMMA; 0000 003B SEMICOLON: 0000 003A COLON