ISO IEC 25436-2006 Information technology - Eiffel Analysis Design and Programming Language《信息技术 Eiffel 分析、设计和程序设计语言》.pdf

1、 Reference number ISO/IEC 25436:2006(E) ISO/IEC 2006INTERNATIONAL STANDARD ISO/IEC 25436 First edition 2006-12-01 Information technology Eiffel: Analysis, Design and Programming Language Technologies de linformation Eiffel: Langage danalyse, conception et programmation ISO/IEC 25436:2006(E) PDF disc

2、laimer 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 this file, parties

3、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 General Info relative to t

4、he 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 below. ISO/IEC 2006 A

5、ll 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 body in the country

6、 of the requester. 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.org Web www.iso.org Published in Switzerland ii ISO/IEC 2006 All rights reservedISO/IEC 25436:2006(E) ISO/IEC 2006 All rights reserved iiiPage 1 Scope 1 1.1 Over

7、view 1 1.2 “The Standard” 1 1.3 Aspects covered 1 1.4 Aspects not covered 1 2 Conformance 2 2.1 Definition2 2.2 Compatibility and non-default options2 2.3 Departure from the Standard .2 3 Normative references .2 3.1 Earlier Eiffel language specifications .2 3.2 Eiffel Kernel Library.2 3.3 Floating p

8、oint number representation.3 3.4 Character set: Unicode 3 3.5 Character set: ASCII 3 3.6 Phonetic alphabet 3 4 Definitions 3 5 Notational conventions 3 5.1 Standard elements .3 5.2 Normative elements .4 5.3 Rules on definitions.4 5.4 Use of defined terms4 5.5 Unfolded forms 5 5.6 Language descriptio

9、n 5 5.7 Validity: “if and only if” rules 5 6 Acronyms and abbreviations .5 6.1 Name of the language 5 6.2 Pronounciation.5 7 General description 6 7.1 Design principles .6 7.2 Object-oriented design 6 7.3 Classes.7 7.4 Types 10 7.5 Assertions 11 7.6 Exceptions .13 7.7 Genericity.14 7.8 Inheritance .

10、15 7.9 Polymorphism and dynamic binding.17 7.10 Combining genericity and inheritance 18 7.11 Deferred classes 19 7.12 Tuples and agents21 7.13 Type- and void-safety.22 7.14 Putting a system together .22 8 Language specification 23 8.1 General organization .23 8.2 Syntax, validity and semantics23 8.2

11、.1 Definition: Syntax, BNF-E23 8.2.2 Definition: Component, construct, specimen 24 8.2.3 Construct Specimen convention.24 8.2.4 Construct Name convention.24 ContentsISO/IEC 25436:2006(E) iv ISO/IEC 2006 All rights reserved8.2.5 Definition: Terminal, non-terminal, token 24 8.2.6 Definition: Productio

12、n 24 8.2.7 Kinds of production25 8.2.8 Definition: Aggregate production25 8.2.9 Definition: Choice production.25 8.2.10 Definition: Repetition production, separator .25 8.2.11 Basic syntax description rule .25 8.2.12 Definition: Non-production syntax rule .26 8.2.13 Textual conventions.26 8.2.14 Def

13、inition: Validity constraint27 8.2.15 Definition: Valid .27 8.2.16 Validity: General Validity rule .27 8.2.17 Definition: Semantics.27 8.2.18 Definition: Execution terminology.27 8.2.19 Semantics: Case Insensitivity principle 27 8.2.20 Definition: Upper name, lower name 28 8.2.21 Syntax (non-product

14、ion): Semicolon Optionality rule 28 8.3 The architecture of Eiffel software 29 8.3.1 Definition: Cluster, subcluster, contains directly, contains.29 8.3.2 Definition: Terminal cluster, internal cluster 29 8.3.3 Definition: Universe .29 8.3.4 Syntax: : Class names.30 8.3.5 Validity: Class Name rule.3

15、0 8.3.6 Semantics: Class name semantics.30 8.3.7 Definition: System, root type name, root procedure name 30 8.3.8 Definition: Type dependency30 8.3.9 Validity: Root Type rule31 8.3.10 Validity: Root Procedure rule .31 8.3.11 Definition: Root type, root procedure, root class.32 8.3.12 Semantics: Syst

16、em execution 32 8.4 Classes.32 8.4.1 Definition: Current class 32 8.4.2 Syntax: : Class declarations 32 8.4.3 Syntax: : Notes32 8.4.4 Semantics: Notes semantics33 8.4.5 Syntax: : Class headers.33 8.4.6 Validity: Class Header rule.33 8.4.7 Definition: Expanded, frozen, deferred, effective class .33 8

17、.4.8 Syntax: : Obsolete marks.34 8.4.9 Semantics: Obsolete semantics.34 8.5 Features .34 8.5.1 Definition: Inherited, immediate; origin; redeclaration; introduce.34 8.5.2 Syntax: : Feature parts 35 8.5.3 Feature categories: overview.35 8.5.4 Syntax: : Feature declarations .35 8.5.5 Syntax: : New fea

18、ture lists .36 8.5.6 Syntax: : Feature bodies36 8.5.7 Validity: Feature Body rule.36 8.5.8 Validity: Definition: Variable attribute37 8.5.10 Definition: Routine, function, procedure .37 8.5.11 Definition: Command, query 37 8.5.12 Definition: Signature, argument signature of a feature27 8.5.13 Featur

19、e principle .38 8.5.14 Syntax: : Feature names38 8.5.15 Syntax (non-production): Alias Syntax rule.38ISO/IEC 25436:2006(E) ISO/IEC 2006 All rights reserved v8.5.16 Definition: Operator feature, bracket feature, identifier-only .39 8.5.17 Definition: Identifier of a feature name .39 8.5.18 Validity:

20、Feature Identifier principle39 8.5.19 Definition: Same feature name, same operator, same alias 39 8.5.20 Syntax: : Operators .40 8.5.21 Syntax: : Assigner marks .40 8.5.22 Validity: Assigner Command rule .40 8.5.23 Definition: Synonym 41 8.5.24 Definition: Unfolded form of a possibly multiple declar

21、ation41 8.5.25 Validity: Feature Declaration rule .42 8.5.26 Validity: Alias Validity rule43 8.6 The inheritance relation.43 8.6.1 Syntax: : Inheritance parts .43 8.6.2 Syntax (non-production): Feature adaptation rule 44 8.6.3 Definition: Parent part for a type, for a class 44 8.6.4 Validity: Class

22、ANY rule .44 8.6.5 Validity: Universal Conformance principle 44 8.6.6 Definition: Unfolded inheritance part of a class 45 8.6.7 Definition: Multiple, single inheritance45 8.6.8 Definition: Inherit, heir, parent45 8.6.9 Definition: Conforming, non-conforming parent 45 8.6.10 Definition: Ancestor type

23、s of a type, of a class.45 8.6.11 Definition: Ancestor, descendant .46 8.6.12 Definition: Proper ancestor, proper descendant .46 8.6.13 Validity: Parent rule .46 8.6.14 Syntax: : Rename clauses .46 8.6.15 Validity: Rename Clause rule.47 8.6.16 Semantics: Renaming principle47 8.6.17 Definition: Final

24、 name, extended final name, final name set.47 8.6.18 Definition: Inherited name48 8.6.19 Definition: Declaration for a feature .48 8.7 Clients and exports 48 8.7.1 Definition: Client relation between classes and types.48 8.7.2 Definition: Client relation between classes.49 8.7.3 Definition: Supplier

25、 49 8.7.4 Definition: Simple client .49 8.7.5 Definition: Expanded client 49 8.7.6 Definition: Generic client, generic supplier .49 8.7.7 Definition: Indirect client 49 8.7.8 Definition: Client set of a Clients part .49 8.7.9 Syntax: : Clients 50 8.7.10 Syntax: : Export adaptation50 8.7.11 Validity:

26、 Export List rule.50 8.7.12 Definition: Client set of a feature .51 8.7.13 Definition: Available for call, available51 8.7.14 Definition: Exported, selectively available, secret.51 8.7.15 Definition: Secret, public property52 8.7.16 Definition: Incremental contract view, short form 52 8.7.17 Definit

27、ion: Contract view, flat-short form 53 8.8 Routines .53 8.8.1 Definition: Formal argument, actual argument53 8.8.2 Syntax: : Formal argument and entity declarations.55 8.8.3 Validity: Formal Argument rule.55 8.8.4 Validity: Entity Declaration rule 54 8.8.5 Syntax: : Routine bodies54ISO/IEC 25436:200

28、6(E) vi ISO/IEC 2006 All rights reserved8.8.6 Definition: Once routine, once procedure, once function 54 8.8.7 Syntax: : Local variable declarations55 8.8.8 Validity: Local Variable rule55 8.8.9 Definition: Local variable .55 8.8.10 Syntax: : Instructions .55 8.9 Correctness and contracts 56 8.9.1 S

29、yntax: : Assertions.56 8.9.2 Syntax (non-production): Assertion Syntax rule56 8.9.3 Definition: Precondition, postcondition, invariant 57 8.9.4 Definition: Contract, subcontract57 8.9.5 Validity: Precondition Export rule .57 8.9.6 Validity: Definition: Availability of an assertion clause 57 8.9.7 Sy

30、ntax: : “Old” postcondition expressions 58 8.9.8 Validity: Old Expression rule 58 8.9.9 Semantics: Old Expression Semantics, associated variable, associated exception marker .58 8.9.10 Semantics: Associated Variable Semantics59 8.9.11 Syntax: : “Only” postcondition clauses .59 8.9.12 Validity: Only

31、Clause rule.59 8.9.13 Definition: Unfolded feature list of an Only clause 60 8.9.14 Definition: Unfolded Only clause 60 8.9.15 Definition: Hoare triple notation (total correctness).60 8.9.16 Semantics: Class consistency60 8.9.17 Syntax: : Check instructions 61 8.9.18 Definition: Check-correct .61 8.

32、9.19 Syntax: : Variants 61 8.9.20 Validity: Variant Expression rule.61 8.9.21 Definition: Loop invariant and variant.61 8.9.22 Definition: Loop-correct .61 8.9.23 Definition: Correctness (class).62 8.9.24 Definition: Local unfolded form of an assertion.62 8.9.25 Semantics: Evaluation of an assertion

33、 .62 8.9.26 Semantics: Assertion monitoring62 8.9.27 Semantics: Assertion violation .63 8.9.28 Semantics: Assertion semantics 63 8.9.29 Semantics: Assertion monitoring levels63 8.10 Feature adaptation .63 8.10.1 Definition: Redeclare, redeclaration .64 8.10.2 Definition: Unfolded form of an assertio

34、n .64 8.10.3 Definition: Assertion extensions.64 8.10.4 Definition: Covariance-aware form of an inherited assertion.64 8.10.5 Definition: Combined precondition, postcondition.65 8.10.6 Definition: Inherited as effective, inherited as deferred.65 8.10.7 Definition: Effect, effecting.65 8.10.8 Definit

35、ion: Redefine, redefinition65 8.10.9 Definition: Name clash.66 8.10.10 Syntax: : Precursor66 8.10.11 Definition: Relative unfolded form of a Precursor. 66 8.10.12 Validity: Precursor rule 66 8.10.13 Definition: Unfolded form of a Precursor . 67 8.10.14 Semantics: Precursor semantics67 8.10.15 Syntax

36、: : Redefinition 67 8.10.16 Validity: Redefine Subclause rule.67 8.10.17 Semantics: Redefinition semantics 67 8.10.18 Syntax: : Undefine clauses 68ISO/IEC 25436:2006(E) ISO/IEC 2006 All rights reserved vii8.10.19 Validity: Undefine Subclause rule 68 8.10.20 Semantics: Undefinition semantics 68 8.10.

37、21 Definition: Effective, deferred feature.68 8.10.22 Definition: Effecting .68 8.10.23 Deferred Class property 68 8.10.24 Effective Class property.68 8.10.25 Definition: Origin, seed 69 8.10.26 Validity: Redeclaration rule 69 8.10.27 Definition: Precursor (joined features)70 8.10.28 Validity: Join

38、rule .70 8.10.29 Semantics: Join Semantics rule.71 8.11 Types 71 8.11.1 Syntax: : Types .71 8.11.2 Semantics: Direct instances and values of a type 72 8.11.3 Semantics: Instances of a type 72 8.11.4 Semantics: Instance principle 72 8.11.5 Definition: Instances, direct instances of a class 72 8.11.6

39、Base principle; base class, base type, based.72 8.11.7 Base rule 73 8.11.8 Validity: Class Type rule 73 8.11.9 Semantics: Type Semantics rule73 8.11.10 Definition: Base class and base type of an expression.73 8.11.11 Semantics: Non-generic class type semantics .74 8.11.12 Definition: Expanded type,

40、reference type74 8.11.13 Definition: Basic type.74 8.11.14 Definition: Anchor, anchored type, anchored entity 74 8.11.15 Definition: Anchor set; cyclic anchor 74 8.11.16 Definition: Types and classes involved in a type 75 8.11.17 Definition: Deanchored form of a type75 8.11.18 Validity: Anchored Typ

41、e rule 75 8.11.19 Definition: Attached, detachable 76 8.11.20 Semantics: Attached type semantics .76 8.11.21 Definition: Stand-alone type.77 8.12 Genericity.77 8.12.1 Syntax: : Actual generic parameters 77 8.12.2 Syntax: : Formal generic parameters .77 8.12.3 Validity: Formal Generic rule77 8.12.4 D

42、efinition: Generic class; constrained, unconstrained 78 8.12.5 Definition: Generic derivation, generic type, non-generic type78 8.12.6 Definition: Self-initializing formal parameter .78 8.12.7 Definition: Constraint, constraining types of a Formal_generic. 78 8.12.8 Syntax: : Generic constraints.78

43、8.12.9 Validity: Generic Constraint rule 79 8.12.10 Definition: Constraining creation features 79 8.12.11 Validity: Generic Derivation rule.79 8.12.12 Definition: Generic-creation-ready type80 8.12.13 Semantics: Generically derived class type semantics.80 8.12.14 Definition: Base type of a single-co

44、nstrained formal generic 80 8.12.15 Definition: Base type of an unconstrained formal generic .81 8.12.16 Definition: Reference or expanded status of a formal generic.81 8.12.17 Definition: Current type81 8.12.18 Definition: Features of a type.81 8.12.19 Definition: Generic substitution 81 8.12.20 Ge

45、neric Type Adaptation rule 81 8.12.21 Definition: Generically constrained feature name .82ISO/IEC 25436:2006(E) viii ISO/IEC 2006 All rights reserved8.12.22 Validity: Multiple Constraints rule .82 8.12.23 Definition: Base type of a multi-constraint formal generic type82 8.13 Tuples .82 8.13.1 Syntax

46、: : Tuple types .82 8.13.2 Syntax: : Manifest tuples .82 8.13.3 Definition: Type sequence of a tuple type.83 8.13.4 Definition: Value sequences associated with a tuple type .83 8.14 Conformance83 8.14.1 Definition: Compatibility between types83 8.14.2 Definition: Compatibility between expressions84

47、8.14.3 Definition: Expression conformance.84 8.14.4 Validity: Signature conformance.84 8.14.5 Definition: Covariant argument 84 8.14.6 Validity: General conformance .85 8.14.7 Definition: Conformance path 85 8.14.8 Validity: Direct conformance: reference types 85 8.14.9 Validity: Direct conformance:

48、 formal generic 86 8.14.10 Validity: Direct conformance: expanded types 86 8.14.11 Validity: Direct conformance: tuple types86 8.15 Convertibility87 8.15.1 Definition: Conversion procedure, conversion type.87 8.15.2 Definition: Conversion query, conversion feature .87 8.15.3 Validity: Conversion pri

49、nciple.87 8.15.4 Validity: Conversion Asymmetry principle.87 8.15.5 Validity: Conversion Non-Transitivity principle87 8.15.6 Syntax: : Converter clauses .87 8.15.7 Validity: Conversion Procedure rule .87 8.15.8 Validity: Conversion Query rule88 8.15.9 Definition: Converting to a class 88 8.15.10 Definition: Converting to and from a type .88 8.15.11 Definition: Converting “through” .88 8.15.12 Semantics: Conversion semantics .89 8.15.13 Definition: Explicit conversion 89 8.15.14 Validity: Expression convertibility .89 8.15.15 Definition: Statically sa