ISO/IEC INTERNATIONAL STANDARD 13568 First edition 2002-07-01 Information technology Z formal specification notation Syntax, type system and semantics Technologies de Il'information Notation Z pour la spécification formelle - Syntaxe, systeme de caracteres et sémantique Reference number ISO/IEC 13568:2002(E) IEC Tso @ISO/IEC2002 py IHS under ted without license from IHS Not for Resale ISO/IEC13568:2002(E) PDF disclaimer This PDF file may contain embedded typefaces. In accordance with Adobe's 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 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 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 ?ISO/IEC2002 Aii rignts reserved. Uniess otherwise specified, no part of this pubication may be reproduced or utilized in any form or by any means, eiectronic or mechanical, including photocopying and microfilm, without permission in writing from either IsO at the address below or IsO's 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 semantic 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 [email protected] Web www.iso.ch Printed in Switzerland ISO/IEC2002-All rights reserved ermittedwithoutlicense from IHS Not for Resale ISO/IEC 13568:2002(E) Contents Page Foreword Introduction vi 1 Scope 2Normative references 3 Terms and definitions 4 Metalanguages 3 5 Conformance 15 6 Z characte 18 7 Lexis 24 8 Concrete syntax 30 9 Characterisation rules 39 10 Annotated synta 40 11 Prelude 43 12Syntactic transformation rules 44 13Type inference rules 55 14 Semantic transformation rules 66 15 Semantic relations 71 Annex A (normative) Mark-ups 79 Annex B (normative) Mathematical toolkit 94 Annex C (normative) Organisation by concrete syntax production 111 Annex D (informative) Tutorial 158 Annex E (informative) Conventions for state-based descriptions 173 Bibliography .175 Index 176 @ISO/IEC 2002—All rights reserved ii Copyright International Organization for Standardization t license from IHS Not for Resale ISO/IEC 13568:2002(E) Figures 1 Phases of the definition 16 B.1 Parent relation between sections of the mathematical toolkit 94 D.1 Concrete parse tree of birthday book example . 161 D.2 Tree of birthday book example after syntactic transformation 164 D.3 Annotated tree of axiomatic example 165 D.4 Annotated tree of generic example 168 D.5 Annotated tree of chained relation example 172 Tables 1 Syntactic metalanguage 3 2 Parentheses in metalanguage 4 3 Propositional connectives in metalanguage 5 4 Quantifiers in metalanguage 5 5 Abbreviations in quantifications in metalanguage 5 6 Conditional expression in metalanguage 5 7 Propositions about sets in metalanguage 9 8 Basic set operations in metalanguage 6 9 Powerset in metalanguage 7 10 Operations on natural numbers in metalanguage 7 11 Decorations of names in metalanguage 7 12 Tuples and Cartesian products in metalanguage 8 13 Function comprehensions in metalanguage 8 14 Relations in metalanguage 8 15 Proposition about relations in metalanguage 8 16 Functions in metalanguage . 6 17 Application in metalanguage 6 18 Sequences in metalanguage 6 19 Disjointness in metalanguage 9 20 Metavariables for phrases 10 21 Metavariables for operator words 11 22