This site contains older material on Eiffel. For the main Eiffel page, see http://www.eiffel.com.

Eiffel: The Reference (Working draft)

This document is a very temporary draft of the current state of "Eiffel: The Reference". It is intended solely for the use of the language committee members of NICE.

The document is generated automatically from the FrameMaker version. The formatting deficiencies are ubiquitous and obvious but the text is there. If there is interest I (BM) will try to continue maintaining this document and, if possible, improve it.

Also of interest: the discussions of the NICE language committee.




Table of Contents

Eiffel:

The Reference Book identification Eiffel: The Reference, ISE Technical Report TR-EI-41/ER. Publication history First published as Eiffel: The Language (TR-EI-2/BR) in 1988. Successive versions appeared in subsequent years and were replaced by TR-EI-17/RM, Eiffel: The Language in 1991, second revised printing 1992, also available as a book published by Prentice Hall, ISBN 0-13-245-925-7. First edition of Eiffel: The Reference under the present report number appeared in 1992. The present revision is 3.3.4, corresponding to version 3.3.4 of the ISE Eiffel environment. It is submitted to the Language Committee of the Nonprofit International Consortium for Eiffel as revision 2 of the proposed Eiffel language standard. The majority of the material in the present book is excerpted from Eiffel: The Language. Author Bertrand Meyer. Software credits See "Credits" at the end of the Preface and in Eiffel: The Language. Cover design Rich Ayling. Copyright notice and proprietary information Copyright \xa9 Bertrand Meyer, 1992, 1995. The material from Eiffel: The Language is reproduced here under permission from copyright holder and the publisher for the exclusive benefit of users of ISE Eiffel 3. In addition, the copyright holder grants permission to members in good standing of the Nonprofit International Consortium for Eiffel to make any use of this document that does not infringe on the rights of other parties, in particular the publisher.

Must it be assumed that because we are engineers beauty is not our concern, and that while we make our constructions robust and durable we do not also strive to make them elegant?

Is it not true that the genuine conditions of strength always comply with the secret conditions of harmony?

The first principle of architectural esthetics is that the essential lines of a monument must be determined by a perfect adaptation to its purpose.

Gustave Eiffel, 1887 From his response in the newspaper Le Temps to a petition by members of the literary and artistic Establishment protesting his project of elevating a tower of iron in Paris. Preface

This document serves two purposes:

  • It is submitted to the Language Committee of the Nonprofit International Consortium for Eiffel as the second step towards a standard definition of Eiffel (the first step was the book Eiffel: The Language).

  • It provides users of Eiffel with a short language definition.

For the first of these goals, note that the present Preface is not part of the intended Standard.

WHAT IS EIFFEL?

The name Eiffel covers a method and a language for the systematic development of quality software, based on the full application of object-oriented principles.

Only the language aspect is covered in this book. Other documents are available on the method and on the various compilers, tools and environments that make it possible to develop software with Eiffel.

A complete description of the Eiffel language has been previously published: the book Eiffel: The Language (Prentice Hall, second printing with corrections, 1992, ISBN 0-13-24795-7). The intent of that document is to provide under a single cover a precise reference, a tutorial, a Guide for the Perplexed, and a detailed user's manual for the language. As a result, much of the space in it is occupied by examples, explanations, justifications, discussions, previews, reminders and comments. ``Eiffel: The Language'' does not shun repetition; occasionally, for example, some part of the discussion needs to refer to the syntax of a construct seen in a distant chapter, and simply reproduces the syntax specification for the convenience of the reader.

In some cases, however, a shorter reference may be necessary. A typical example is that of someone implementing an Eiffel compiler, who may be presumed to be familiar with the rationale behind the various components of the language, but will need a document were he can quickly find precise answers to specific questions, often on fine points (``Can the target of an anchored declaration be anchored too?''). Another example is that of a user who is familiar with the language but wants to keep a concise reference on his desk.

Providing such a no-frills description of Eiffel is the purpose of Eiffel: The Reference. 

-----------------------------------------------------------------------------
This book is not meant as a first introduction to Eiffel. If you do not know
the language, or know it only superficially, you should read Eiffel: The
Language. The present book will mostly be useful as a summary of Eiffel:
The Language for readers who are familiar with that earlier book.
-----------------------------------------------------------------------------

THE SHORT FORM

The worst that could happen to the description of Eiffel is to follow the fate of so many earlier languages: the emergence of several descriptions, each slightly incompatible with the others. Eiffel: The Language went to considerable length to prevent this from happening. By threading several levels of discourse into a single cloth, the book was able to forestall eventual divergence.

In particular, the book relied on an extensive system of ``road signs'' to identify each of the interwoven threads: syntax, validity, semantics, comment, caveat, preview, reminder.

As this system is directly reflected in the source electronic form of the original document, it is possible to use software tools, aided by a little human intervention, to extract one or several of the threads. This approach is what made the present book possible. It is not, strictly speaking, a new book, but an extract of the relevant parts of Eiffel: The Language.

Another way of expressing this observation is to claim that producing this book was, to a certain extent, a software project: writing the tools that would extract the essential parts of the complete document and ignore the rest. This effort required some ``massaging'', as programmers say, of the original text, to mark some parts as retained and others as discarded. But the extent of that massaging was remarkably limited: the text was organized in such a systematic way that most of the extraction could be done automatically, based on a number of selection rules not unlike those of a little expert systems.

Anyone familiar with the Eiffel method will have recognized the idea: it is the notion of short form. To document an Eiffel class, you do not as a rule write a separate document; you should instead include the relevant information in the class text itself, and rely on computer tools to extract views of the class at various levels of abstraction, in particular the short (or flat-short) form which only keeps the interface properties of the class -- signatures, preconditions, postconditions and header comments of exported features, class invariant -- while discarding the implementation information (non-exported features, routine bodies, distinction between functions and attributes). Here we are doing the same with respect to the language itself: using the power of the computer to remove the non-essential information from a complete description.

The major advantage, in the case of classes, is that we can keep a single description. So when things evolve -- as they inevitably will, be they classes or languages -- we have only one document to maintain. This may be called the principle of single reference and is essential to the smooth evolution of the language and its description.

Although the work of the NICE library committee may cause changes to be brought to the present document independently of Eiffel: The Language, every effort will be made to maintain the principle of single reference, avoiding the disaster that divergence between the two documents would mean for Eiffel. In particular, the structure and section numbering will be kept the same for the two books, and changes made to the present one as a result of the committee's work will be continuously reflected back into the electronic version of Eiffel: The Language.

LIBRARY ELEMENTS

The definition of Eiffel relies on a number of predefined classes in the "Kernel Library", covering such fundamental notions as basic types (BOOLEAN, INTEGER and the like), arrays, input and output.

A preliminary standard document for the Kernel Library, known as the PELKS (Proposed Eiffel Library Kernel Standard) is currently under study by NICE. To avoid any ambiguity or contradiction, all discussions of Kernel Library classes in this book have been replaced by references to the PELKS.

CHANGES

This book correspnds to the second printing of Eiffel: The Language. It incorporates a few corrections corresponding to mistakes that have been detected since the publication of the book. The principal among these changes are listed in chapter 14 of ISE Eiffel: The Environment (Technical Report TR-39/IE).

A complete list of the changes will be made available separately. Time prevented inclusion of change bars for the first release of this document, but they will be part of future editions; all changes have been carefully logged.

In case of discrepancy between Eiffel: The Language and Eiffel: The Reference, follow the document that has the latest printing date, unless the problem appears to be due to a text processing mistake. Remember that at the basis of Eiffel there is only one document; the only differences result from how one selects and prints portions of that document. This is the required condition for the stability, maturity and credibility of the Eiffel language; in other words, for its success.

The present book uses the same conventions as Eiffel: The Language. To avoid any confusion, the original chapter and section numbers have been retained. So if you have leafed through this book before reading the present preface, you may have wondered why the first chapter is number 2 and its first section 2.2; but the purpose is clear: making it easy to find the corresponding place in Eiffel: The Language if when examining some part of the edifice you want to retrieve the scaffolding --- in other words some of the supporting comments and examples. Using a different section numbering scheme for the present book would have caused endless misunderstandings.

Unlike the sections, the pages have been renumbered, since consecutive numbering facilitates searching for specific information.

In contrast with Eiffel: The Language, this book avoids repetition of any kind. This is why you will find no syntax summary or syntax diagram. Such elements (which are present in the complete description) will be easy to add if readers feel they are necessary.

There is currently no index, but this omission will be repaired in a future version.

Finally, please remember that the present edition is only the second release of Eiffel: The Reference. In particular, some errors may remain in the software that served to extract the information and produce the index. Indulgence is thus requested from the reader.

ACKNOWLEDGMENTS

In addition to the acknowledgments included at the end of the preface to Eiffel: The Language, it is appropriate to thank the various readers who have contributed comments since the book's publication, most remarkably David Hollenberg from the Information Systems Institute of the University of Southern California and Helmut Weber from Austria, formerly from IBM. 2 Syntax, validity and semantics

2 Syntax, validity and semantics

2.2 SYNTAX, COMPONENTS, SPECIMENS AND CONSTRUCTS

Eiffel's syntax is the set of rules describing the structure of class texts. It covers neither limitations on valid texts (described by validity constraints) nor the execution-time meaning or effect of these texts (described by semantic rules). Definition: component Any class text, or syntactically meaningful part of that text, such as an instruction, an expression or an identifier, is called a component. Definition: construct, specimen The structure of any components is described by a construct. A component conforming to a certain construct is called a specimen of that construct. For example, the construct Class describes the structure of class texts; any particular class text, built according to the rules given in this book, is a specimen of this construct.

All constructs have names beginning with a capital letter and written in the default (roman) font. Each appears in the index with a reference to the page of its syntactical definition.

An important convention will simplify the discussions: the phrase ``an X'', where X is the name of a construct, serves as a shorthand for ``a specimen of construct X''. For example, ``a Class'' means ``a specimen of construct Class'', in other words a text built according to the syntactical specification of construct Class.

2.3 TERMINALS, NON-TERMINALS AND TOKENS

Every construct is either a ``terminal'' or a ``non-terminal'' as defined next. Definitions: Terminal, Non-terminal, Token Specimens of a terminal construct have no further syntactical structure. Examples include reserved words (such as class, Result etc.), constants such as integers, and identifiers used to denote classes, features and entities. In contrast, the specimens of a non-terminal construct are defined in terms of other constructs. Definition: token, lexical component The specimens of terminal constructs are called tokens or lexical components. They form the basic vocabulary out of which you may build more complex texts --- specimens of non-terminals.

2.4 PRODUCTIONS

Definition: production

To understand a non-terminal, you need a formal description of the structure of its specimens. Such a description is called the production for the construct.

A production has the form

Construct right-hand-side

Every non-terminal construct appears on the left-hand side of exactly one such production. The symbol means ``is defined as''.

The right-hand-side of the production describes the structure of specimens of the left-hand-side construct. Three forms of right-hand-side are available:

  • Aggregate, describing a construct made of a fixed number of parts (some of which may be optional) to be concatenated in a given order.

  • Choice, describing a construct having a number of given variants.

  • Repetition, describing a construct made of a variable number of parts, which are all specimens of a given construct.

An aggregate right-hand-side is a non-empty sequence of constructs, some of which may be in square brackets [ ] to indicate optional parts.

A choice right-hand side is a non-empty sequence of constructs separated by vertical bars | .

A repetition right-hand side is of one of the two forms {Construct § ...} {Construct § ...} +

where §, the separator, is some construct --- usually, but not necessarily, terminal. Appearing in a production for a left-hand side construct R, this states that a specimen of R consists of zero or more specimens of B, separated, if more than one, by the separator §. In the first form, without a +, specimens of R may be empty; in the second form, with a +, they must include at least one B.

2.6 VALIDITY

The productions and other elements labeled , as described so far, specify the structure of constructs. Definition: validity constraint, valid Supplementary requirements on the syntactically well-formed specimens of a construct are called validity constraints on the construct. Paragraphs introducing them are labeled by the VALIDITY road sign.

A specimen which follows the syntactic rules and satisfies the constraints will be accepted by the language processing tools of any Eiffel environment and is said to be valid.

Every validity constraint has a four-character code beginning with V (shown as VVVV in the above fictitious example).

2.7 INTERPRETING THE CONSTRAINTS

General Validity rule

Every validity constraint relative to a construct is considered to include an implicit supplementary condition stating that every component of the construct satisfies every validity constraint applicable to the component.

2.8 SEMANTICS

A construct specimen which is syntactically legal and valid has an associated semantics, specifying its run-time effect in a system in which the specimen appears. That semantics may include executing certain actions, producing a value, or both. It is defined by the paragraphs. For specimens made of further components, the specification usually refers recursively to the components' own semantics.

It is important to remember that the SEMANTICS paragraphs only apply to valid specimens. In many cases, the semantic rules would not even make sense otherwise. Clearly, attempting to describe the effect of an invalid component would be useless.

2.9 CORRECTNESS

Validity is only a structural property; valid Eiffel software is not guaranteed to perform according to any expected behavior. In fact, execution of valid software may lead to non-termination, or to exceptions and eventual failure.

For a valid component, then, we need a more advanced criterion: its ability to operate properly at run-time. This is called correctness and is a more elusive aim than validity, since it involves semantic properties.

2.10 THE CONTEXT OF EXECUTING SYSTEMS

Definitions: run time, machine, platform, language processing tool

The following terminology will serve to discuss the context of system execution:

  • Run time is the period during which a system is executed.

  • The machine is the combination of hardware (one or more computers) and operating system which makes it possible to execute systems.

  • The machine type, that is to say a certain kind of computer and a certain operating system, is called a platform.

  • To make the text of an Eiffel system executable by a machine, you will need software tools such as compilers and interpreters, for which this book will use the term language processing tool, general enough to cover various implementation techniques.

2.11 REQUIREMENTS ON LANGUAGE PROCESSING TOOLS

The definition of Eiffel syntax, validity and semantics contained in this book is also a specification of certain aspects of the corresponding language processing tools.

Not all aspects apply to all language processing tools.

A language processing tool that processes software components at a certain level (syntax, validity, semantics) is not required to perform the tasks associated with that level on components which do not not satisfy the requirements at the previous levels.

In almost all cases, authors of tools should follow a stricter guideline and make sure that their tools reject any input that does not satisfy the rules applying to the earlier levels. Such rejection should include a clear error message. For syntax, the message should identify the production which is not properly observed; for validity it should give the code of the violated validity constraint (and the clause number for constraints divided into clauses).

Two special considerations may justify occasional departures from this general obligation of rejection: A semantic tool may be able to process valid parts of a text, even if other parts are invalid. For example, a compiler may generate code for some valid classes in a system, rejecting classes which are not valid.
A tool author may have a particular reason for providing a tool or tool option which accepts input violating a specific validity constraint. A possible application would be for a prototyping mode which attempts to execute incomplete systems, or skips certain checks. Such tool variants are outside of the semantics of Eiffel proper and should be clearly labeled as such, reminding developers that acceptance of an input text provides no guarantee that the text satisfies the full language rules.

One final note, intended for implementors of Eiffel, and regarding what they might not find here. Although this book goes to great lengths to include every relevant validity and semantic property, it may of course have left an occasional one out. Such an oversight might be a case of incompleteness (a missing validity constraint or semantic specification) or inconsistency (ambiguous or contradictory answers).

If you run into such a case while trying to produce language processing tools, please contact the language committee of NICE by sending electronic mail to <language-chair @nice.twr.com>, 3 The architecture of Eiffel software

3 The architecture of Eiffel software

3.1 OVERVIEW

The constituents of Eiffel software are called classes. By extracting classes from a given universe, you may assemble them into executable systems. To keep your classes and your development organized, it is convenient to group classes into clusters.

These four concepts provide the basis for structuring Eiffel software:

  • A class is a modular unit.

  • A system results from the assembly of one or more classes to produce an executable unit.

  • A cluster is a set of related classes.

  • A universe is a set of clusters, out of which developers will pick classes to build systems.

Of these, only ``class'', describing the basic building blocks, corresponds directly to a construct of the language. To build systems out of classes, you will use not a language mechanism, but tools of the supporting environment. As to clusters and universes, they are not language constructs but mechanisms for grouping and storing classes using the facilities provided by the underlying operating system, such as files and directories.

3.3 CLASS TEXTS AND CLASS NAMES

Every class has a name, such as DOCUMENT or PARAGRAPH, and a class text which describes the features of the class and its other properties.

For class names, as for all uses of identifiers, letter case is not significant: identifiers such as DOCUMENT, document and even dOcUmEnT have the same semantics when viewed as class names. Definition: Upper Name The standard recommended style in Eiffel texts is to write all class names using exclusively the upper name of the class, that is to say the name all in upper case (such as DOCUMENT). Definition: Class Name The term ``class name'' as used in this book denotes the upper name of a class. In particular, two classes are said to have the same class name if they have the same case-independent names, even if the names are written with different case conventions in the class texts.

3.4 SYSTEMS

Definition: System, Root A system is a set of classes, one of which has been designated as the root of the system, such that all the classes on which the root depends belong to the system. Definition: Dependency Here a class C is said to depend on a class A if one of the following holds:

  • C is an heir of A.

  • C is a client of A.

  • Recursively, there is a class B such that C depends on B and B depends on A.
Root Class rule

A class C may be used as root of a system if and only if it satisfies the following three conditions:

  1. C is not generic.
    C is not deferred.
    Any creation procedure of C has either no formal argument, or a single formal argument of type ARRAY [STRING].

3.5 CLUSTERS

Definition: Cluster A cluster is a set of classes, all with different names.

No two classes in a given cluster may have the same class name.

3.6 UNIVERSES

Definition: Universe A universe is a set of clusters. 4 Classes

4 Classes

4.2 OBJECTS

Definitions: object, instance Viewed as a type, a class describes the properties of a set of possible data structures, or objects, which may exist during the execution of a system that includes the class; these objects are called the instances of the class.

4.3 FEATURES

Definitions: feature, attribute, routine Viewed as a module, a class introduces, through its class text, a set of features. Some features, called attributes, represent fields of the class's direct instances; others, called routines, represent computations applicable to those instances. .lY Since there is no other modular facility than the class, building a software system in Eiffel means analyzing the types of objects the system will manipulate, and writing a class for each of these types.

4.5 CLASS TEXT STRUCTURE

-----------------------------------------------------
Class_declaration  (fig)  [Indexing]
                          Class_header
                          [Formal_generics]
                          [Obsolete]
                          [Inheritance]
                          [Creators]
                          [Features]
                          [Invariant]
                          end ["--" class Class_name]
-----------------------------------------------------

4.7 INDEXING A CLASS

---------------------------------------------------
Indexing      (fig)  indexing Index_list
Index_list    (fig)  {Index_clause ";" ...}
Index_clause  (fig)  [Index] Index_terms
Index         (fig)  Identifier ":"
Index_terms   (fig)  {Index_value "," ...} +
Index_value   (fig)  Identifier | Manifest_constant
---------------------------------------------------

The Indexing clause has no effect on the execution semantics.

4.8 CLASS HEADER

---------------------------------------------------
Class_header  (fig)  [Header_mark] class Class_name
Header_mark   (fig)  deferred | expanded
Class_name    (fig)  Identifier
---------------------------------------------------

A Class_header appearing in the text of a class C is valid if and only if it satisfies either of the following two conditions:

There is no header mark of the deferred form, and C is effective.
There is a Header_mark of the deferred form, and C is deferred.

4.9 FORMAL GENERIC PARAMETERS

------------------------------------------------------------
Formal_generics      (fig)  "[" Formal_generic_list "]"
Formal_generic_list  (fig)  {Formal_generic ","...}
Formal_generic       (fig)  Formal_generic_name [Constraint]
Formal_generic_name  (fig)  Identifier
Constraint           (fig)  "-->" Class_type
------------------------------------------------------------

A Formal_generics part of a Class_declaration is valid if and only if every Formal_generic_name G appearing in it satisfies the following three conditions:

G is different from the name of any class in the surrounding universe.
G is different from any other Formal_generic_name appearing in the same Formal_generics_part.
If a Constraint is given, it does not involve any types other than class names and formal generic parameters other than G itself.

4.10 OBSOLETE CLAUSE

---------------------------------
Obsolete  (fig)  obsolete Message
Message   (fig)  Manifest_string
---------------------------------

Declaring a class as Obsolete does not affect its semantics. But some language processing tools should produce a warning when they process a class that relies, as client or descendant, on an obsolete class. The warning should include the Message.

4.11 ENDING COMMENT

If present, the ending comment must repeat the Class_name given at the head of the class.

5 Features

5 Features

5.3 IMMEDIATE AND INHERITED FEATURES

Definitions: features of a class, inherited, origin, introduced The features of a class C include its inherited features and its immediate features, defined as follows: The features obtained by C from its parents, if any, are its inherited features.
In the Features part of C, consider a declaration describing a feature f. If f is inherited, the declaration is in fact a redeclaration of f, giving f new properties in C. If this is not the case, f is a new feature, said to be immediate in C. C is then the class of origin (or simply ``origin'') of f, which is also said to be introduced in C.

5.6 FEATURES PART: SYNTAX

-----------------------------------------------------------------------
Features                  (fig)  feature {Feature_clause feature ...} +
Feature_clause            (fig)  [Clients]
                                 [Header_comment]
                                 Feature_declaration_list
Feature_declaration_list  (fig)  {Feature_declaration ";" ...}
Header_comment            (fig)  Comment
-----------------------------------------------------------------------

5.7 FORMS OF FEATURES

Every feature of a class is either an attribute or a routine. Definition: field By introducing an attribute in a class, you specify that at run-time every instance of the class will possess a certain value, or field, corresponding to the attribute.

An attribute is either variable or constant:

  • If an attribute is variable, the corresponding fields may be different for various instances of the class and may change at run-time. As a consequence, the actual values must be stored in the representation of each instance.

  • If an attribute is constant, the corresponding field is the same value for all instances, and may not change at run-time. This value appears in the class as part of the attribute declaration.

By introducing a routine in a class, you specify that a certain computation (an algorithm) must be applicable to instances of the class.

A routine is either a procedure or a function:

  • A procedure does not return a result; it may perform a number of operations, some of which may modify the instance to which the procedure is applied.

  • A function returns a result and may also perform operations.

5.9 FEATURE DECLARATIONS: SYNTAX

----------------------------------------------------------------
Feature_declaration  (fig)  New_feature_list Declaration_body
Declaration_body     (fig)  [Formal_arguments]
                            [Type_mark]
                            [Constant_or_routine]
Constant_or_routine  (fig)  is Feature_value
Feature_value        (fig)  Manifest_constant | Unique | Routine
----------------------------------------------------------------

5.10 COMPONENTS OF A FEATURE DECLARATION

------------------------------------------------
New_feature_list  (fig)  {New_feature "," ...} +
New_feature       (fig)  [frozen] Feature_name
------------------------------------------------

5.11 HOW TO RECOGNIZE FEATURES

A Feature_declaration is a variable attribute declaration if and only if it satisfies the following conditions:

  • There is no Formal_arguments part.

  • There is a Type_mark part.

  • There is no Constant_or_routine part.

A Feature_declaration is a constant attribute declaration if and only if it satisfies the following conditions:

  • There is no Formal_arguments part.

  • There is a Type_mark part.

  • There is a Constant_or_routine part, which contains either a Manifest_constant or a Unique.

A Feature_declaration is a routine declaration if and only if it satisfies the following condition:

  • There is a Constant_or_routine part, whose Feature_value is a Routine.

In this case the Formal_arguments and Type_mark parts may or may not be present. If the Type_mark is present, the declaration describes a function; otherwise it describes a procedure.

5.12 THE SIGNATURE OF A FEATURE

Definition: signature The signature of a feature f is a pair <argument_types, result_type> where both argument_types and result_type are sequences of types, defined as follows.

  • If f is a routine, argument_types is the possibly empty sequence of the types of its arguments. If f is an attribute, argument_types is an empty sequence.

  • If f is an attribute or a function, result_type is a one-element sequence, whose single element is the type of f. If f is a procedure, f is an empty sequence.
Definition: argument signature The first component of a feature's signature, written argument_types in this definition, is called the argument signature of the feature. The argument signature gives the types of the feature's arguments; it is an empty sequence for attributes and for routines without arguments.

5.13 FEATURE NAMES

------------------------------------------------------
Feature_name     (fig)  Identifier | Prefix | Infix
Prefix           (fig)  prefix '"' Prefix_operator '"'
Infix            (fig)  infix '"' Infix_operator '"'
Prefix_operator  (fig)  Unary | Free_operator
Infix_operator   (fig)  Binary | Free_operator
------------------------------------------------------
Definition: identifier feature, operator feature A feature declared with an identifier is called an identifier feature. A feature declared with an operator is called an operator feature. 

--------------------------------------------
Unary   (fig)  not | "+" | "\-"
Binary  (fig)  "+" | "--" | "*" | "^" |
               "<" | ">" | "<=" | ">=" |
               "//" | "\\" | "^" |
               and | or | xor |
               and then | or else | implies
--------------------------------------------
Definition: same feature name By convention, two feature names are the same if and only if either of the following conditions holds:

  • They are both identifier features, with identical lower name.

  • They are both operator features, both Prefix or both Infix, with identical lower names.

5.14 VALIDITY OF FEATURE DECLARATIONS

Feature Declaration rule

A Feature_declaration appearing in a class C, and whose New_feature_list contains one or more feature names f1, ..., fn, is valid if and only if it satisfies all of the following conditions:

  • Its Declaration_body describes a feature which, according to the rules of 5.11, is one of: variable attribute, constant attribute, procedure, function.

  • None of the fi has the same name as another feature introduced in C (in particular, fi is not the same name as fj for different i and j).

  • If the name of any of the fi is the same as the final name of any inherited feature, the Declaration_body satisfies the Redeclaration rule.

  • If the Declaration_body describes a deferred feature, then none of the fi is preceded by the keyword frozen.

  • If any of the fi is a Prefix name, the Declaration_body describes an attribute or a function with no argument.

  • If any of the fi is an Infix name, the Declaration_body describes a function with exactly one argument.

  • If the Declaration_body describes a once function, the result type involves neither a Formal_generic_name nor an Anchored type.

5.16 SYNONYMS

Multiple Declaration rule

The semantics of a feature declaration applying to more than one feature name, as in

f1, f2, ... , fn some_declaration_body

is (except in one special case) defined as the semantics of the corresponding sequence of declarations naming only one feature each, and with identical declaration bodies, as in: f1 some_declaration_body; f2 some_declaration_body; ... fn some_declaration_body

The special case is that of a multiple declaration introducing Unique constant attributes, which is covered by the Unique Declaration rule.

5.17 OBSOLETE FEATURES

Declaring a routine as Obsolete does not affect its semantics. But language processing tools, or at least some of them, should produce a warning when they process a client or descendant class that uses the routine. The warning should include the Message.

6 The inheritance relation

6 The inheritance relation

6.2 AN INHERITANCE PART

Definition: multiple, single inheritance Multiple inheritance occurs as soon as there is more than one Parent clause (even if they all refer to the same parent class, a case called repeated inheritance and studied in chapter 11).

6.3 FORM OF THE INHERITANCE PART

----------------------------------------------------------
Inheritance         (fig)  inherit Parent_list
.xk inherit
Parent_list         (fig)  {Parent ";" ...}
Parent              (fig)  Class_type [Feature_adaptation]
Feature_adaptation  (fig)  [Rename]
                           [New_exports]
                           [Undefine]
                           [Redefine]
                           [Select]
                           end
----------------------------------------------------------
Definition: parent clause for a class The Parent_list names a number of Parent clauses. Each Parent clause is relative to a Class_type, that is to say a class name B possibly followed by actual generic parameters (as in B [T, U]). B must be the name of a class in the universe to which the current class belongs. The clause is said to be a ``Parent clause for B''.

6.4 RELATIONS INDUCED BY INHERITANCE

Definition: heir, parent If class C has a Parent clause for B, then C is said to inherit from B; B is said to be a parent of C, and C is said to be an heir of B. Definition: ancestor, descendant Class A is an ancestor of class B if and only if A is B itself or, recursively, an ancestor of one of B's parents. Class B is a descendant of class A if and only if A is an ancestor of B, in other words if B is A or (recursively) a descendant of one of its heirs. Definition: proper ancestor, descendant The proper ancestors of a class C are its ancestors other than C itself. The proper descendants of a class B are its descendants other than B itself.

6.6 THE INHERITANCE STRUCTURE

Parent rule

The Inheritance clause of a class D is valid if and only if it meets the following two conditions:

In every Parent clause for a class B, B is not a descendant of D.
If two or more Parent clauses are for classes which have a common ancestor A, D meets the conditions of the Repeated Inheritance Consistency constraint for A.

6.9 RENAMING

------------------------------------------------
Rename       (fig)  rename Rename_list
Rename_list  (fig)  {Rename_pair "," ...}
Rename_pair  (fig)  Feature_name as Feature_name
------------------------------------------------

Rename Clause rule

A Rename_pair of the form old_name as new_name, appearing in the Rename subclause of the Parent clause for B in a class C, is valid if and only if it satisfies the following five conditions:

old_name is the final name of a feature f of B.
old_name does not appear as the first element of any other Rename_pair in the same Rename subclause.
new_name satisfies the Feature Name rule for C.
If new_name is of the Prefix form, f is an attribute or a function with no argument.
If new_name is of the Infix form, f is a function with one argument.

Renaming does not affect the semantics of an inherited feature, but simply gives it a new final name in an heir, as defined below.

6.10 FEATURES AND THEIR NAMES

Definition: name of a feature in a class Within the text of a class C, any feature f of C is accessible through a feature name, known as the name of f in C. As this expression suggests, the association between a feature and a feature name is not absolute but relative to a class. The same feature may well be denoted by different names in different classes. Definition: original name The original name of a feature is the name under which it is declared in its class of origin. Definition: final name Every feature f of a class C has a final name in C, defined as follows:

  • If f is immediate in C, its final name is its original name

  • If f is inherited, f is obtained from a feature of a parent B of C. Let parent_name be (recursively) the final name of that feature in B. Then:

  • If the Parent clause for B in C contains a Rename_pair of the form rename parent_name as new_name, the final name of f in C is new_name. Otherwise, the final name is parent_name.
Definition: final name set The final names of all the features of a class constitute the final name set of a class. Definition: inherited name The inherited name of a feature obtained from a feature f of a parent B is the final name of f in B. Definition: name of a feature In this book, references to the ``name'' of a feature, if not further qualified, always denote the final name.

6.11 INHERITANCE AND EXPANSION

The only consequence of the expansion status of a class is the semantics of entities of the corresponding types, such as x above. An expanded class may inherit from an non-expanded one, and conversely. The expansion status is not transmitted under inheritance; it is entirely determined by the presence or absence of the expanded mark in the class's own Class_header, not by any property of its parents.

6.12 ANY

Any class other than GENERAL and ANY which does not include an explicitly written Inheritance clause is considered to have an implicit clause of the form

inherit ANY

6.15 PROVIDING YOUR OWN UNIVERSAL CLASS

Whether you use the default ANY or another one, any system will need to have a class of name ANY. This is a constraint on any valid universe.

7 Clients and exports

7 Clients and exports

7.3 CONVENTIONS

Definition: client A class C is a client of S if some ancestor of C is a simple client, an expanded client or a generic client of S. Definition: client relation between classes A class C is a client of a class B if C is a client of a type whose base class is B. A class C is a direct or indirect client of a type S of base type B if there is a sequence of classes C1 = A, C2, ..., Cn = B such that n > 1 and every Ci is a client of Ci+1 for 1 <= i <= n. The ``direct or indirect'' forms of the simple client, expanded client and generic client relations are defined similarly.

7.4 SIMPLE CLIENTS

Definition: simple client A class C is a simple client of a type S if some entity or expression of C is of type S.

7.5 EXPANDED CLIENTS

Definition: expanded client A class C is an expanded client of a type S if S is an expanded type and some attribute of C is of type S.

Expanded Client rule

It is valid for a class C to be an expanded client of a class SC if and only if SC is not a direct or indirect expanded client of C.

7.6 GENERIC CLIENTS

Definition: generic client, generic supplier A class C is a generic client of a type S if for some generically derived type T of the form B [..., S, ...] one of the following holds: C is a client of T.
One of the Parent clauses of C, or of a proper ancestor of C, lists T as parent.

7.12 THE EXPORT STATUS OF FEATURES

Definition: exported, selectively available The status of a feature of a class is one of the following: The feature may be available to all classes. Such a feature is said to be exported, of generally available.
The feature may be available to specific classes only. In that case it is also available to the descendants of all these classes. Such a feature is said to be selectively available to the given classes and their descendants.
The feature may be available to no classes. Then it is said to be secret.
Definition: available A feature of a class S is said to be available to a class C if and only if it is either selectively available to S or generally available.

7.13 ADAPTING THE EXPORT STATUS

---------------------------------------
Clients     (fig)  "{" Class_list "}"
Class_list  (fig)  {Class_name "," ...}
---------------------------------------

A Clients part is valid if and only if every Class_name appearing in its Class_list is the name of a class in the surrounding universe. 

-------------------------------------------------
New_exports      (fig)  export New_export_list
New_export_list  (fig)  {New_export_item ";" ...}
New_export_item  (fig)  Clients Feature_set
Feature_set      (fig)  Feature_list | all
Feature_list     (fig)  {Feature_name "," ...}
-------------------------------------------------

Export List rule

A New_exports parent appearing in class C in a Parent clause for a parent B, of the form

export {class_list1} feature_list1; ... {class_listn} feature_listn

is valid if and only if (for i in the interval 1..n): At most one of the feature_listi is the keyword all.
All the other feature_listi are lists of final names of features of C obtained from B.
No final feature name appears twice in any such list, or appears in more than one list.

An immediate feature of a class has the following export status:

  • If the Feature_clause which introduces it has no Clients part (that is to say, begins with the keyword feature with no further qualification), the feature is exported (generally available).

  • If the Feature_clause which introduces it has a Clients part (that is to say, begins with feature {A, B, C ...}), the feature is selectively available to the descendants of the classes listed in that Clients part, and to these descendants only.
Definition: secret If a Feature_clause has an empty Clients list, that is to say, begins with feature {}, then the features it introduces are secret.

If a non-redeclared inherited feature f has more than one precursor, it is available to all classes to which it would be available as a consequence of applying the preceding rule separately to each of its precursors.

7.14 DESCRIBING A CLASS FOR CLIENTS: THE SHORT FORM

Definition: short form, abstract form The short form of a class, also called its abstract form, is a text which has the same structure as the class but does not include non-public elements. The short form is the one that should be used as interface documentation for the class.

7.15 THE FLAT-SHORT FORM

Definition: flat-short form The flat-short form of a class is similar to the short form, but applies to the ``reconstructed'' full text of a class; you may view it as resulting from a shortening step that has been preceded by a ``flattening'' step, which expands the class text to unfold all the features obtained from proper ancestors, putting them at the same level as the immediate features of the class. Clearly, flattening must take both renaming and redefinition into account. 8 Routines

8 Routines

8.3 FORMAL ARGUMENTS

-------------------------------------------------------------------
Formal_arguments          (fig)  "(" Entity_declaration_list ")"
Entity_declaration_list   (fig)  {Entity_declaration_group ";" ...}
Entity_declaration_group  (fig)  Identifier_list Type_mark
Identifier_list           (fig)  {Identifier "," ...}+
Type_mark                 (fig)  ":" Type
-------------------------------------------------------------------

Formal Argument rule

Let fa be the Formal_arguments part of a routine r in a class C. Let formals be the concatenation of every Identifier_list of every Entity_declaration_group in fa. Then fa is valid if and only if no Identifier e appearing in formals is the final name of a feature of C.

Let el be an Entity_declaration_list. Let identifiers be the concatenation of every Identifier_list of every Entity_declaration_group in fa. Then el is valid if and only if no Identifier appears more than once in the list identifiers.

8.5 ROUTINE STRUCTURE

---------------------------------------
Routine  (fig)  [Obsolete]
                [Header_comment]
                [Precondition]
                [Local_declarations]
                Routine_body
                [Postcondition]
                [Rescue]
                end ["--" Feature_name]
---------------------------------------

Routine rule

A Routine part of a routine declaration is valid if and only if one of the following conditions holds: Its Routine_body is an Internal body (beginning with do or once).
In the other cases (where the Routine_body is External or Deferred), there is neither a Local_declarations part nor a Rescue part.

8.6 ROUTINE BODY

------------------------------------------
Routine_body  (fig)  Effective | Deferred
Effective     (fig)  Internal | External
Internal      (fig)  Routine_mark Compound
Routine_mark  (fig)  do | once
Deferred      (fig)  deferred
------------------------------------------

The introductory keywords do or once of an Internal body correspond to different semantics for calls to the routine:

For a do body, as indicated above, the initialization and body are executed anew on each call.
If routine o of class C has a once body (o is then called a ``once routine''), the initialization and body of o are executed only for the first call to o applied to an instance of C during any given session. For every subsequent call to o applied to an instance of C during the same session, the routine call has no effect; if the routine is a function, the value it returns is the same as the value returned by the first call.

8.7 LOCAL ENTITIES AND Result

--------------------------------------------------------
Local_declarations  (fig)  local Entity_declaration_list
--------------------------------------------------------

Local Entity rule

Let ld be the Local_declarations part of a routine r in a class C. Let locals be the concatenation of every Identifier_list of every Entity_declaration_group in ld. Then ld is valid if and only if every Identifier e in ld satisfies the following two conditions:

No feature of C has e as its final name.
No formal argument of r has e as its Identifier.
Definition: local entity Most of the rules governing the validity and semantics of declared local entities also apply to a special predefined entity: Result, which may only appear in the Routine_body or Postcondition of a function, and denotes the result to be returned by the function. Reflecting this similarity, this book uses the term "local entity" to cover Result as well as declared local entities.

8.9 TYPES OF INSTRUCTIONS

--------------------------------------------------------
Instruction  (fig)  Creation |
                    Call |
                    Assignment |
                    Assignment_attempt |
                    Conditional | Multi_branch | Loop |
                    Debug | Check | Retry
--------------------------------------------------------
9 Correctness

9 Correctness

9.5 FORM OF ASSERTIONS

---------------------------------------------------------
Precondition          (fig)  require [else] Assertion
Postcondition         (fig)  ensure [then] Assertion
Invariant             (fig)  invariant Assertion
Assertion             (fig)  {Assertion_clause ";" ...}
Assertion_clause      (fig)  [Tag_mark]
                             Unlabeled_assertion_clause
Unlabeled_assertion_  (fig)  Boolean_expression | Comment
clause
Tag_mark              (fig)  Tag ":"
Tag                   (fig)  Identifier
---------------------------------------------------------

In an Assertion, the semicolon separating each Assertion from the next has the same semantics as the and then infix boolean operator. This means that the order of the clauses may be meaningful:

The value of an Assertion is true if and only if every Assertion_clause in the Assertion has value true.
If an Assertion_clause has value false, the whole Assertion in which it appears has value false, even if the value of a subsequent clause is not defined.

9.7 THE SPECIFICATION OF A ROUTINE

Definition: specification, subspecification Let pre and post be the precondition and postcondition of a routine rout. The specification of rout is the pair of assertions <pre, post>. A specification <pre', post'> is said to be a subspecification of <pre, post> if and only if pre implies pre' and post' implies post. Here ``implies'' is boolean implication.

9.8 CONSTRAINTS ON ROUTINE ASSERTIONS

A Precondition of a routine r of a class C is valid if and only if every feature whose final name appears in any Assertion_clause is available to every class to which r is available.

Definition: availability of an assertion clause An Assertion_clause a of a routine Precondition or Postcondition is available to a class B if and only if all the entities involved in a are available to B, with the convention that formal arguments and Result are available to all classes.

9.9 OLD EXPRESSION

--------------------------
Old  (fig)  old Expression
--------------------------

An Old expression of the form old e, where e is an expression of type TE, is valid if and only if it satisfies the following two conditions:

It appears in a Postcondition clause of a Routine r.
Transforming r into a function with result type TE (by adding a result type if r is procedure, or changing its result type if it is already a function) and replacing its entire Routine part by do Result := e end would yield a valid routine.

The value of an Old expression old e is defined only at the end of the execution of a call to r, just before the call returns; it is the result that would have been produced by evaluating e just before the call's execution began.

9.11 CLASS INVARIANTS

Definition: invariant of a class The invariant of a class C is an assertion obtained by concatenating the following assertions (omitting any one which is absent or empty): The invariants of all parents (determined recursively through the present rule), in the order of the corresponding Parent clauses.
The postconditions of any inherited functions which C redefines as an attribute, with every occurrence of Result replaced by the attribute's final name. (If there are two or more such redefinitions, include them in the order in which their new declarations appear in C.)
The Assertion in C's own Invariant clause, if any.

9.12 CONSISTENCY OF A CLASS

Definition: consistency A class C is consistent if and only if it satisfies the following two conditions: For every creation procedure p of C: {prep} dop {INVC & postp}
For every routine r of C exported generally or selectively:
{prer & INVC} dor {postr & INVC}

In this rule, INVC is the invariant of C and, for any routine s, pres is the precondition of s, posts its postcondition, and dos its body.

9.13 CHECK INSTRUCTIONS

---------------------------------
Check  (fig)  check Assertion end
---------------------------------
Definition: check-correct An effective routine r is check-correct if, for every Check instruction c in r, any execution of c (as part of an execution of r) satisfies all its assertions.

9.14 LOOP INVARIANTS AND VARIANTS 

---------------------------------------------
Variant  (fig)  variant [Tag_mark] Expression
---------------------------------------------

A Variant is valid if and only if its Expression is of type INTEGER.

The invariant assertion INV of a loop must have the following two properties:

  • The loop's Initialization (from clause) ensures the truth of INV.

  • Any execution of the Loop_body, when started in a state that does not satisfy the Exit_condition, preserves the truth of INV (in other words, leaves INV true if it finds INV originally true).
Definition: loop-correct A routine is loop-correct if every loop it contains satisfies the following four conditions:

  1. {true} INIT {INV}
    {true} INIT {VAR >= 0}
    {INV and then not EXIT} BODY {INV}
    {INV and then not EXIT and then (VAR = v)} BODY {0 <= VAR < v}
where INV is the loop's invariant, VAR its variant, INIT its Initialization, EXIT its Exit condition, and BODY its Loop_body.

9.16 CORRECTNES S OF A CLASS

Definition: correctness (class) A class is correct if and only if it is consistent and every routine of the class is check-correct, loop-correct and exception-correct.

9.17 SEMANTICS OF ASSERTIONS

For a correct system, assertions, in all cases, will have no effect on the semantics of system execution (except through possible side effects of the functions called by assertions). For an incorrect system, the effect depends on compilation or execution options. Various options of the environment will make it possible to evaluate assertions. If an assertion evaluates to true, it has no further effect on the outcome of the computation. If it evaluates to false, it will trigger an exception, disrupting the normal flow of computation, as discussed in the chapter on exception handling.

An assertion violation detected as a result of enabling assertion monitoring at one of the above levels triggers an exception. An exception will also result, at level loop or higher, if a loop iteration fails to decrease the variant or gives it a negative value.

Here is the rule for determining the recipient of an exception resulting from an assertion violation:

For postconditions, class invariants, loop invariants, variants and Check instructions, the recipient is the routine whose text contains the violated assertion or variant.
For a violated precondition, the recipient is the calling routine. In this case no component of the routine's body is executed; the routine fails immediately, not performing any of its normal actions, and triggering an exception in the caller.
10 Feature adaptation

10 Feature adaptation

10.2 REDECLARING INHERITED FEATURES: WHY AND HOW

Definition: redeclaration A class that contains a redefinition or effecting of an inherited feature will be said to redeclare that feature.

10.6 THE REDEFINITION CLAUSE

Definition: precursor If a class inherits a feature from a parent, either keeping the feature unchanged or redefining it, the parent's version of the feature is called the precursor of the feature.

10.15 REDECLARATION AND ASSERTIONS

Consider a routine redeclaration and let pre1, ... pren be the precursors' preconditions and post1, ..., postn be the precursors' postconditions. Assume that new assertion clauses are present, of the form:

require else alternative_precondition

ensure then extra_postcondition

Then the redeclared routine will be considered to have the precondition and postcondition

alternative_precondition or else pre1 or else ... or else pren

extra_postcondition and then post1 and then ... and then postn

If, in a routine redeclaration, the Precondition part is absent, the redeclared routine is considered to have false as its alternative_precondition; if the Postcondition part is absent, the redeclared routine is considered to have true as its extra_postcondition. Because of the rules of boolean algebra, the absence of one of these assertions means that the corresponding precursor assertion is kept as it was. (Or-ing a boolean value with false, or and-ing it with true, does not change the condition.)

For a declaration of an immediate feature of a class, the require else form of Precondition clause has the same meaning as if it were introduced by just require, and the ensure then form of Postcondition clause has the same meaning as if it were introduced by just ensure.

10.16 UNDEFINING A FEATURE

Definition: inherited as effective, as deferred In the rest of this discussion, an inherited feature is said to be inherited as effective if it has at least one effective precursor and the corresponding Parent part does not undefine it. Otherwise the feature is inherited as deferred.

10.17 THE JOIN MECHANISM

If C inherits and joins two or more deferred features, the net result for C is as if it had inherited a single deferred feature. In the absence of further action from C, that feature remains deferred. Of course, C may also provide an effective declaration for the feature, killing several abstract birds with one concrete stone by using a single redeclaration to effect several features inherited as deferred.

10.19 REDEFINITION AND UNDEFINITION RULES

---------------------------------------
Redefine  (fig)  redefine Feature_list
Undefine  (fig)  undefine Feature_list
---------------------------------------

Redefine Subclause rule

Consider a class C with a parent B. If a Parent part for B in C contains a Redefine subclause, that clause is valid if and only if every Feature_identifier fname that it lists (in its Feature_list) satisfies the following conditions:

  1. fname is the final name in C of a feature inherited from B.
    That feature was not frozen, and was not a constant attribute.
    fname appears only once in the Feature_list.
    The Features part of C contains oneFeature_declaration for fname, which is a valid redeclaration, but not an effecting, of the original feature.

The effect of redefining a feature in a class is that any use of the feature in the class, its clients or (barring further redefinitions) its proper descendants will refer to the redefined version rather than the original.

Undefine Subclause rule

Consider a class C that inherits from a class B. If a Parent part for B in C contains an Undefine subclause, that clause is valid if and only if, for every Feature_identifier fname that it lists (in its Feature_list): fname is the final name in C of a feature inherited from B.
That feature was not frozen, and was not an attribute.
That feature was effective in B.
fname appears only once in the Feature_list.

10.20 DEFERRED AND EFFECTIVE FEATURES AND CLASSES

Definition: effective feature, deferred feature, effecting A feature f of a class C is said to be an effective feature of C if and only if any of the following conditions holds. f is introduced in C as an attribute or a routine whose Routine_body is of the Effective form (that is to say, not the keyword deferred but beginning with do, once or external).
f is an inherited feature, coming from a parent B of C where it is (recursively) effective, and C does not undefine it.
Another feature of C with the same final name is (recursively) effective. That feature is then said to effect f in C.

A feature of C is a deferred feature of C if and only if it is not an effective feature of C.

Condition 3 defines the effecting case: an effective feature, which has the same final name as one or more deferred features, serves as effecting for all of them.

Definition: deferred, effective class A class is deferred if it has at least one deferred feature. It is effective otherwise.

10.21 ORIGIN AND SEED

Definition: origin, seed

Every feature of a class C has a seed, which is a feature, and an origin, which is a class, defined as follows. Any immediate feature of C (in other words, any feature introduced in C rather than inherited) is its own seed, and has C as its origin.
An inherited feature of C with two or more precursors, all of which have (recursively) the same seed s, also has s as its seed. (This is the case of sharing under repeated inheritance.)
If C joins a set of inherited deferred features, yielding (as explained above) a single feature of C to which case 2 does not apply, that feature is its own seed and its origin is C.
Any feature of C to which none of the previous cases applies is inherited, and has exactly one precursor; then its seed and origin are (recursively) the seed and origin of that precursor.

10.22 REDECLARATION RULES

Definition: redeclaration, redefinition, effecting

A class C redeclares an inherited feature f if and only if one of the following two conditions holds:

  • C contains a Feature_declaration for a feature g with the same final name as f.

  • C inherits f as deferred, and inherits as effective another feature g with the same final name as f.

A redefinition is a redeclaration which is not an effecting.

Redeclaration rule

Let C be a class and g a feature of C. It is valid for g to be a redeclaration of a feature f inherited from a parent B of C if and only if the following conditions are satisfied. No effective feature of C other than f and g has the same final name.
The signature of g conforms to the signature of f.
If g is a routine, its Precondition, if any, begins with require else (not just require), and its Postcondition, if any, begins with ensure then (not just ensure).
If the redeclaration is a redefinition (rather than an effecting) the Redefine subclause of the Parent part for B lists the final name of f in its Feature_list.
If f is inherited as effective, then g is also effective.
If f is an attribute, g is an attribute, f and g are both variable, and their types are either both expanded or both non-expanded.
If either one of f and g is an External routine, so is the other.
Definition: declared type

Any feature or entity of a class C has a declared type as follows:

  • For a feature which is immediate in C or redeclared in C, dt is the type given by the declaration or redeclaration.

  • For an inherited feature which is not redeclared in C, dt is (recursively) the declared type of its precursors in the corresponding parents.

  • For the predefined entity Current, dt is C with its formal generic parameters if any.

  • For the predefined entity Result, appearing in a function, dt is the return type declared for the function.

  • For any other entity e, dt is the type used in the declaration of e.
Definition: type of a feature In this book, the ``type'' of a feature or entity, without further qualification, always means its declared type (rather than its base type).

10.23 RULES ON JOINING FEATURES

Definition: precursor (joined features) A precursor of an inherited feature is a version of the feature in the parent from which it is inherited. Without the join mechanism there was just one precursor; but a feature which results from the join of two or more deferred features will have all of them as precursors.

Join rule

It is valid for a class C to inherit two different features as deferred under the same final name if and only if, after possible redeclaration in C, they have identical signatures.

Join Semantics rule

Joining deferred features with the same final name yields a non-obsolete deferred feature defined as follows:

Its name is the final name of all its precursors.
Its signature is the precursors' signature, which the Join rule indicates must be the same for all precursors after possible redeclaration.
Its precondition is the or of all the precursors' preconditions.
Its postcondition is the and of all the precursors' postconditions.
Its Header_comment is the concatenation of those of all precursors.
It is not obsolete (even if some of the precursors are obsolete).
11 Repeated inheritance

11 Repeated inheritance

11.2 CASES OF REPEATED INHERITANCE

Definition: repeated inheritance, ancestor, descendant Repeated inheritance occurs whenever (as a result of multiple inheritance) two or more of the ancestors of a class D have a common parent A. D is then called a repeated descendant of A, and A a repeated ancestor of D. Definition: direct repeated inheritance The simplest case, called direct repeated inheritance, corresponds to the following scheme (where D is a ``repeated heir'' of A): class D inherit A rename ... redefine ... end; A rename ... redefine ... end ... Rest of class omitted ... Definition: indirect repeated inheritance The second case, indirect repeated inheritance, arises when one parent of D is a proper descendant of A, and one or more other parents are descendants of A. (Some of the paths may be direct.)

11.3 SHARING AND REPLICATION

Repeated Inheritance rule

Let D be a class and B1, ... Bn (n >= 2) be parents of D having a common ancestor A. Let f1, ... fn be features of these respective parents, all having as their seed the same feature f of A. Then: Any subset of these features inherited by D under the same final name yields a single feature of D.
Any two of these features inherited under a different name yield two features of D.
Definition: shared, replicated Features will be said to be shared if case 1 of the Repeated Inheritance rule applies, and replicated if case 2 applies.

11.10 NAME CLASHES

Definition: name clash

A name clash occurs for a certain feature name fname in a class C if, for two different parents A and B of C, both A and B have a feature of name fname.

11.11 THE INHERITED FEATURES OF A CLASS

Definition: inherited features

Let D be a class. The list inherited of inherited features of D is obtained as follows. Let precursors be the list obtained by concatenating the lists of features of every parent of D; this list may contain duplicates in the case of repeated inheritance. Then inherited is obtained from precursors as follows: In list precursors, for any set of two or more elements representing features that are repeatedly inherited in D under the same name, so that the Repeated Inheritance rule yields sharing, keep only one of these elements. The Repeated Inheritance Consistency constraint (sharing case) indicates that these elements must all represent the same feature, so that it does not matter which one is kept.
For every feature f in the resulting list, if D undefines f, replace f by a deferred feature with the same signature and specification.
In the resulting list, for any set of deferred features with the same final name in D, keep only one of these features, with assertions joined as per the Join Semantics rule. (Keep the signature, which the Join rule requires to be the same for all the features involved.)
In the resulting list, remove any deferred feature such that there is an effective feature with the same final name in the list. (This is the case in which a feature f inherited as effective effects one or more deferred features: of the whole group, only f remains.)
Let merged_features be the resulting list. All its elements have different feature names; they are the inherited features of D in their parent form. From this list, produce a new one as follows: for any feature which D redeclares (by redefinition or effecting), replace the feature by the result of the redeclaration; keep any other feature as it is in merged_features.
The result is the list inherited of inherited features of D.

Feature Name rule

It is valid for a class C to introduce a feature with the Feature_name fname, or to inherit a feature under the final name fname, if and only if no other feature of C has that same name. A class may not introduce two different features, both deferred or both effective, with the same name.
If a class introduces a feature with the same name as a feature it inherits in effective form, it must rename the inherited version.
If a class inherits two features as effective from different parents and they have the same name, the class must also (except under sharing for repeated inheritance) remove the name clash through renaming.

11.12 VERSIONS OF A FEATURE

Definition: potential version Let f be a feature of a class A and D a descendant of A. A potential version of f in D is any inherited feature of D which is either:

  • f itself.

  • A feature resulting (recursively) from a redeclaration of a potential version of f.

  • (Recursively) a potential version of a feature of which f is a redeclaration.

  • A feature resulting (recursively) from a generic derivation of A.
Definition: version Let f be a feature of a class A and D a descendant of A. The version of f in D is the feature df defined as follows: If D has only one potential version of f, then df is that feature.
If D has two or more potential versions of f, the Repeated Inheritance Consistency constraint, seen below, states that exactly one of them must appear, under its final D name, as part of a Select clause in D; then df is that feature.
Definition: potentially ambiguous Let D be a repeated descendant of a class A. A feature f of A is potentially ambiguous in D if and only if one of the following two conditions holds: f is an attribute.
D has two or more potential versions of f.

11.13 THE REPEATED INHERITANCE CONSISTENCY CONSTRAINT

----------------------------------
Select  (fig)  select Feature_list
----------------------------------

It is valid for a class D to be a repeated descendant of a class A if and only if D satisfies the following two conditions for every feature f of A:

If the Repeated Inheritance rule implies that f will be shared in D, then all the inherited versions of f are the same feature.
If the Repeated Inheritance rule implies that f will be replicated in D and f is potentially ambiguous, then the Select subclause of exactly one of the Parent parts of D lists the corresponding version of f, under its final D name.

Select Subclause rule

A Select subclause appearing in the Parent part for a class B in a class D is valid if and only if, for every Feature_name fname in its Feature_list, fname is the final name in D of a feature that has two or more potential versions in D, and fname appears only once in the Feature_list.

12 Types

12 Types

12.4 HOW TO DECLARE A TYPE 

--------------------------------------------------------
Type                 (fig)  Class_type |
                            Class_type_expanded |
                            Formal_generic_name |
                            Anchored |
                            Bit_type
Class_type           (fig)  Class_name [Actual_generics]
Actual_generics      (fig)  "[" Type_list "]"
Type_list            (fig)  {Type "," ...}
Class_type_expanded  (fig)  expanded Class_type
Bit_type             (fig)  BIT Constant
Anchored             (fig)  like Anchor
Anchor               (fig)  Identifier | Current
--------------------------------------------------------

12.5 BASE CLASS, BASE TYPE

Class Type rule

An Identifier CC is valid as the Class_name part of a Class_type if and only if it is the name of a class in the surrounding universe.

12.7 UNCONSTRAINED GENERICITY

Definition: base class, base type (class Type) The base class of a generically derived type is the class used to derive it by providing actual generic parameters. Definition: constrained, unconstrained generic The syntax for Class_declaration includes an optional Constraint part after every formal generic parameter. If present, this part makes the parameter constrained; if not, the parameter is unconstrained. A generic class is constrained if it has at least one constrained parameter, unconstrained otherwise. Definition: generic class, generic derivation, non-generic Any class declared with a non-empty Formal_generics part (constrained or not) is said to be a generic class. A generic class does not describe a type but a template for a set of possible types. To derive an actual type from this template, you must provide an Actual_generics list, whose elements are themselves types. The result is called a generic derivation.

Unconstrained Genericity rule

Let CT be a Class_type having a non-empty Actual_generics part, whose base class C is not a constrained generic class. CT is valid if and only if C satisfies the following two conditions: C is a generic class.
The number of Type components in CT's Actual_generics list is the same as the number of Formal_generic parameters in the Formal_generic_list of C's declaration.

A generically derived type is expanded if its base class is an expanded class; otherwise it is a reference type.

12.8 CONSTRAINED GENERICITY

The effect of a Constraint, if present, is to restrict allowable actual generic parameters to types that conform to the Class_type given.

Constrained Genericity rule

Let C be a constrained generic class. A Class_type CT having C as base class is valid if and only if CT satisfies the two conditions of the Unconstrained Genericity rule (VTUG, page \n(Qt) and, in addition: For any Formal_generic parameter in the declaration of C having a constraint of the form --> D, the corresponding Type in the Actual_generics list of CT conforms to D.

12.9 USING FORMAL GENERIC PARAMETERS AS TYPES

Definition: base class, base type (constrained generic) We consider the base type of a constrained generic parameter to be its constraining type, with the associated base class. Definition: base class, base type (unconstrained generic) ANY serves as both the base type and the base class of any unconstrained Formal_generic_name.

12.11 CLASS TYPES EXPANDED

If T is a valid Class_type, generically derived or not, expanded T is a valid Class_type_expanded, and the possible values for entities of that type are instances of T.

12.12 RULES ON EXPANDED TYPES

Definition: expanded type, reference type A type T is expanded if and only if one of the following conditions holds: T is a Class_type whose base class C is an expanded class.
T is of the form expanded CT. (As noted, it is redundant but not erroneous for the base class of CT to be an expanded class.)
T is of the form BIT M for some non-negative integer M.
T is a reference type if it is not a Formal_generic_name and none of the above condition applies.

Expanded Type rule

It is valid to use an expanded type of base class C in the text of a class B if and only if it satisfies the following two conditions: C is not a deferred class.
C either has no Creators part, or has a Creators part containing exactly one creation procedure, with no argument, available to B for creation.

Any entity declared of an expanded type has run-time values which are instances of the corresponding base type.

12.14 BIT TYPES

A Bit_type declaration is valid if and only if its Constant is of type INTEGER, and has a positive value.

The possible values of an entity declared as BIT N for some N are bit sequences of exactly N bits.

12.15 ANCHORED TYPES

Definition: anchored type, anchor An Anchored type is of the form

like anchor where anchor is called the anchor of the type.

An anchored type of the form like anchor appearing in a class C is valid if and only if one of the following holds:

anchor is the final name of an attribute or function of C, whose declared type is a non-Anchored reference type.
The type appears in the text of a routine r of C, and anchor is a formal argument of r, whose declared type is a non-Anchored reference type.
anchor is the reserved word Current.

The base type BT of an anchored type like anchor appearing in a class C is determined as follows:

Definition: base class, base type (anchored) If anchor is the final name of some feature of C, then BT is the declared type of that feature in C.
If anchor is a formal routine argument, then BT is the type declared for that argument in the Formal_arguments list.
If anchor is Current, then BT is C followed by its Formal_generics, if any, with any Constraint removed.
13 Conformance

13 Conformance

13.3 SIGNATURE CONFORMANCE

A signature t = (<B1, ..., Bn>, <S>) conforms to a signature s = (<A1, ..., An>, <R>) if and only if it satisfies the following conditions:

Each of the two sequence components of t has the same number of elements as the corresponding component of s.
Every type Ti in each of the two sequence components of t conforms to the corresponding type Si in the corresponding component of s.

13.4 DIRECT AND INDIRECT CONFORMANCE

Let T and V be two types. V conforms to T if and only if one of the following holds:

V and T are identical.
V conforms directly to T.
V is NONE and T is a reference type.
V is B [Y1,... Yn] for some generic class B, T is B [X1,... Xn], and every one of the Yi conforms (recursively) to the corresponding Xi.
T is a reference type and, for some type U, V conforms to U and U conforms (recursively) to T.

13.5 CONFORMANCE TO A NON-GENERIC REFERENCE TYPE

Let CT be a Class_type of base class C, and BT be a reference type whose base class B is not generic. CT conforms directly to BT if and only if the Inheritance clause of C lists B in one or more of its Parent items.

13.6 GENERICALLY DERIVED REFERENCE TYPES

Let BT be a generically derived reference type of base type B [X1,... Xn] for some n >= 1, where the formal generic parameters of B are G1,... Gn. Let CT be a Class_type of base class C different from B. To determine whether CT conforms directly to BT, define the substitution σas follows:

  • If CT is non-generic, σ is the identity substitution.

  • If CT is a a generically derived type, of the form C [Y1,... Ym], and class C is declared with formal generic parameters H1,... Hm, then σ applied to any of the Hi (for 1 <= i <= m) is Yi, and σ applied to any other element is the element itself.

Then CT conforms directly to BT if and only if the Inheritance clause of C lists B [Z1,... Zn] as one of its Parent items and, for every j such that 1 <= j <= n, applying substitution σ to Zj yields Xj.

13.7 FORMAL GENERIC PARAMETERS

Let G be a formal generic parameter of a class, which in the class may be used as a type of the Formal_generic_name category. No type conforms directly to G. If G is not constrained, it conforms directly to the type ANY (based on the corresponding universal class) and to no other type. If G is constrained by CT, G conforms directly to CT and to no other type.

13.8 ANCHORED TYPES

In a class C, type like Current conforms directly to its base type CT, where CT is C followed by its Formal_generic_list, if any, with any Constraint removed.

Type like anchor, where anchor is a feature of C or a formal argument of a routine of C, conforms directly to the type of anchor in C.

An anchored type conforms directly to no type other than implied by these rules. No type conforms directly to an anchored type.

13.9 EXPRESSION CONFORMANCE

An expression v of type VT conforms to an expression t of type TT if and only if they satisfy any one of the following four conditions.

VT conforms to TT.
TT is like v (v in this case must be an entity).
VT and TT are both of the form like x for the same x.
TT is like x where x is a formal argument to a routine r, v is an actual argument in a call to r, and VT conforms to the type of the actual argument corresponding to x in the call.
v is a call to some function f of type like x where x is a formal argument of f, and the type of the actual argument corresponding to x in the call conforms to TT.

13.10 EXPANDED TYPES

Definition: heavier arithmetic type Any arithmetic type conforms to heavier ones, where DOUBLE is heavier than REAL and INTEGER, and REAL is heavier than INTEGER.

Let T be an expanded type other than a Bit_type. A type U conforms directly to T if and only if they satisfy any one of the following three conditions:

T is of the form expanded BT, and U is BT.
T is REAL and U is INTEGER.
T is DOUBLE and U is REAL or INTEGER.

In case 1 T also conforms directly to U.

An expanded type conforms directly to no type other than implied by this rule and the rules of 13.5 and 13.6.

13.11 BIT TYPES

The possible direct conformance cases involving a Bit_type are the following for any positive integers N and P:

BIT N conforms directly to ANY.
BIT N conforms directly to BIT P for N <= P.

Other than implied by these rules, no type conforms directly to a Bit_type, and a Bit_type conforms directly to no type. 14 Control structures

14 Control structures

14.2 COMPOUND

--------------------------------------
Compound  (fig)  {Instruction ";" ...}
--------------------------------------

The effect of executing a Compound may be defined as follows.

  • If the Compound has zero instructions, the effect is to leave the state of the computation unchanged.

  • If the Compound has one or more instructions, its effect is that of executing the first instruction of the Compound and then (recursively) to execute the Compound obtained by removing the first instruction.

14.3 NULL INSTRUCTION

Specimens of the null instruction are empty.

The effect of the null instruction is to leave the state of the computation unchanged.

14.4 CONDITIONAL 

--------------------------------------------------------
Conditional     (fig)  if Then_part_list [Else_part] end
Then_part_list  (fig)  {Then_part elseif ...}+
Then_part       (fig)  Boolean_expression then Compound
Else_part       (fig)  else Compound
--------------------------------------------------------

To define precisely the semantics of this construct, a few auxiliary notions are useful. As the syntactical specification shows, a Conditional begins with

if condition1 then compound1

where condition1 is a boolean expression and compound1 is a Compound. Definition: secondary part The remaining part may optionally begin with elseif. If so, replacing the first elseif by if would transform the remaining part into a new, syntactically correct, Conditional; such an instruction is called the secondary part of the enclosing Conditional.

The final part, also optional, is of the form else compoundn. Definition: prevail immediately If the value of condition1 is true when the instruction is executed, then the Conditional is said to prevail immediately.

Finally, we may consider that every Conditional has an Else_part if we understand an empty Else_part to stand for one with an empty Compound.

With these conventions, the effect of a Conditional may be defined as follows. If the Conditional prevails immediately, then its effect is that of its compound1 part, as defined above. Otherwise:

  • If it has a secondary part, the effect of the entire Conditional is (recursively) the effect of the secondary part.

  • If it has no secondary part, its effect is that of the (possibly empty) Compound in its Else part.

14.5 MULTI-BRANCH CHOICE

Definition: inspect expression A Multi_branch instruction contains a Expression, called the inspect expression, appearing after the keyword inspect. The inspect expression, last_input in the example, may only be of type INTEGER or, as here, CHARACTER. It includes one or more When_part, each of which indicates a list of one or more Choice, separated by commas, and a Compound to be executed when the value of the Expression is one of the given Choice values. Definition: inspect constant Every Choice specifies one or more values, called inspect constants. More precisely, a Choice is either a single constant (Manifest_constant or