Path: utzoo!utgpu!jarvis.csri.toronto.edu!rutgers!tut.cis.ohio-state.edu!ucsd!hub!eiffel!bertrand From: bertrand@eiffel.UUCP (Bertrand Meyer) Newsgroups: comp.lang.eiffel Subject: Static typing for Eiffel Keywords: The full paper - PART 2 (of 2). Message-ID: <177@eiffel.UUCP> Date: 10 Jul 89 22:29:06 GMT Organization: Interactive Software Engineering, Santa Barbara CA Lines: 879 Because its size is > 50K, this article has been split into two parts for posting to Usenet. Please make sure you have both parts. THIS IS THE BEGINNING OF PART 2 (OF 2) 4 RATIONALE FOR THE EIFFEL RULES Before studying the solution, we will pause to consider the Eiffel type rules giving rise to the above problems and assess whether they make sense from a software engineering perspective. These rules have indeed been criticized [1, 3, 4] (the second of these references even includes a rather baroque proposal for ``fixing'' these rules). Several related messages have also been posted to the comp.lang.eiffel newsgroup. These rules were not designed hastily, however, and the experience of several years and hundreds of thousands of lines of useful Eiffel software even suggests that they are the only acceptable ones. 4.1 Rationale for the export rule Consider first the export-inheritance rule, which often surprises newcomers as an apparent violation of information hiding principles. How can a descendant override export restrictions of an ancestor, or hide what the ancestor exported? To obtain a better perspective on this rule it is useful to examine its application to what may be the archetypal example of inheritance. Assume PARENT is a class POLYGON and HEIR is a class RECTANGLE. The inheritance relation in this case is clear and natural. It is not absurd, however, to assume that class POLYGON has a procedure add_vertex (new: POINT) is -- Insert new vertex new at current cursor position do ... ensure nb_vertices = old nb_vertices + 1 end -- add_vertex For general polygons, this procedure may make sense. It is not, however, applicable to rectangles, whose class invariant should contain the clause nb_vertices = 4 The Eiffel solution is to ensure that class RECTANGLE does not export procedure add_vertex. This is the kind of case that led to situations such as /1/, with f being add_vertex. POLYGON ^ ^ / \ / \ / \ / \ / \ / \ FIXED_POLYGON VARIABLE_POLYGON ^ feature | add_vertices | | | | | RECTANGLE invariant nb_vertices = 4 Figure 1 : Alternative inheritance structures Three policies are possible in the face of such cases. + Policy 1 considers that this use of inheritance is inadequate: RECTANGLE is not a subtype of POLYGON because not all operations applicable to the latter are applicable to the former. According to this policy, the proper solution (see figure 1) is to consider two heirs to POLYGON: FIXED_POLYGON and VARIABLE_POLYGON. Procedure add_vertex is a feature of VARIABLE_POLYGON only, whereas RECTANGLE inherits from FIXED_POLYGON. This way the Eiffel rule can be changed to require that every class should export all features exported by its ancestors. (Even with this policy, however, there is no reason to prohibit a class from exporting a feature hidden by a proper ancestor. This technique is commonly used in practical Eiffel programming and, as discussed above, entails no danger of type failure.) + Policy 2 considers that inheritance is used properly in this case, but only for half of its capacity: as a module enrichment mechanism, not as a subtyping facility. The definition of class RECTANGLE should be permitted, but not polymorphic assignments of the form p := r (with p of type POLYGON and r of type RECTANGLE). The conformance rules governing such assignments (as given in section 11.3.1 of [5]) should be updated to exclude such cases. If polymorphic assignments are needed, then the inheritance structure should be redesigned as shown in figure 1. + Policy 3 is more liberal: it permits the above polymorphic assignments as long as it can be ascertained statically at reasonable cost, for any Eiffel system involving these classes, that no type failure may result; in other words, that no add_vertex operation may ever be applied to p or an entity that may become associated with p. This is the policy applied in Eiffel, for which the exact rules will be given below. What speaks in favor of policies 1 and 2 is that they are extremely easy to implement for the compiler writer. Restricting exports in descendant classes (policy 1) is trivial; restricting polymorphic aliasing (policy 2) is almost as immediate. These solutions would also have the advantage of quieting the theoreticians and removing the fears of prospective users. In short, all obvious arguments seemed to push the designers of Eiffel towards policy 1 or 2: convenience (since the same group is also in charge of an implementation) and ease of convincing future users. So it takes some dose of courage to choose policy 3 and stick to it. Why should this be the Eiffel policy? The reasons can only be understood by going beyond the purely theoretical discussions and considering the practice of object-oriented software construction. Policies 1 and 2 assume that programming is for gods. Gods never make any mistake. Those among them who aside from their other business indulge in the heavenly pleasures of object-oriented programming always get their inheritance structures right the first time around. In today's job market, however, most employers must resort to hiring programmers who are only demigods, or even in some cases (although they will deny it) mere mortals. Then we have to accept the need to work with inheritance structures that may already in be place and have been designed with less-than-perfect foresight. Assume for example that POLYGON had already been designed and has descendants such as CONVEX_POLYGON and CONCAVE_POLYGON. In other words, the existing inheritance structure does not take into account the difference between ``variable'' and ``fixed'' polygons. Then a new programmer comes in and has a need for RECTANGLE; writing it as an heir to POLYGON seems the obvious solution. Policy 1 precludes doing this without first reorganizing the entire inheritance structure. This is unrealistic in a practical development environment. True, we should accept the need for regular improvements of inheritance structures, reflecting improved understanding of software artefacts. But as anyone who has managed a class library in an industrial environment will appreciate, such evolution should be carefully planned and properly controlled. One cannot accept a situation in which new but legitimate uses of a class require constant changes in the design of existing libraries. Policy 2 is only marginally better. It does allow the programmer to define RECTANGLE as an heir to POLYGON but prevents him from using polymorphism in this case; it is not possible, for example, to define a data structure such as polygon_stack: STACK [POLYGON] and push a RECTANGLE object onto polygon_stack. This is particularly frustrating in an application that never even uses add_vertex. Again, the only solution is to redesign the inheritance structure. Policies 1 and 2 are overly inflexible. In contrast, the idea of policy 3 is to avoid bothering programmers with unnecessary restrictions when their use of inheritance cannot possibly lead to any type failure. The criterion to apply is obvious in the example given: the checker should reject any software system that contains both of the operations + p := r + p.add_vertex (...) Because checkers cannot realistically carry out flow analysis, it is not necessary to check whether or not these two instructions can be executed on the same control flow path; the mere presence of both in the same system is reason enough for the checker to reject that system. In other words, we accept without regret that the following sequence (with n an integer entity) will be rejected even though it cannot possibly lead to a type failure: if n >= 0 then p := r end if n < 0 then p.add_vertex (...) end The reason for this was discussed in section 2.4: checkers should only be bound to perform ``reasonable'' controls. For a checker to recognize that the above is safe requires control flow analysis, whose cost, if it is at all possible, is not justified by the benefit. Using the terminology of section 2.4, we are past the point of diminishing returns. As noted, type checking is always a pessimistic strategy; the only question is what degree of pessimism is acceptable. Rejecting extracts of the above form appears acceptable because it is hard to conceive of them being used in useful programs. This is not true, however, of the much stronger pessimism implied by policies 1 and 2, which leads to rejection of programs that, for the reasons discussed above, are useful and even needed. How policy 3 can be implemented at reasonable cost will be discussed below. 4.2 Further reflections on inheritance The argument made above for orthogonal export and inheritance mechanisms was that inheritance structures may be temporarily imperfect. The implied consequence is that eventually these structures will be perfected; then policies 1 and 2 could be implemented if we were willing to implement tougher library management procedures (forcing restructuring when appropriate, and requiring new heir designs to wait in the meantime). Unfortunately, even such an approach may not be viable. In practice we must probably accept that some inheritance structures will always be imperfect. Inheritance is the application to software engineering of the most fundamental of all scientific techniques: classification. The modern forms of the natural sciences, since Linnaeus, and of mathematics, at least since Bourbaki, were borne out of systematic efforts to classify natural and artificial objects; object-oriented programming attempts the same for software objects. Classification is humanity's attempt to bring a semblance of order to the description of an otherwise rather chaotic world. As anyone who has ever tried to use a botany book to recognize actual flowers knows, classifications never quite achieve perfection. Close as one can get to a fully satisfactory system, a few exceptions and special examples will remain. Moving from botany to zoology, the cliche' example of ostriches and flying illustrates these problems well. In class BIRD, it seems appropriate to include and export a feature fly. But a descendant class such as STRUTHIO (the name of the genus that includes ostriches) should not export fly. This is really the Eiffel form of selective inheritance, or rejecting part of your heritage: the rejected feature is still there internally, but not visible by your clients. (The discussion of selective inheritance in section 10.5.3 of [5], is too restrictive in this respect: it seems to reject any form of selective inheritance, even though Eiffel supports the form discussed here.) In a case such as this one there does not seem to be a much better solution. Any other classification of birds, for example into flying and non-flying ones, would miss key criteria for distinguishing between various classes of birds, and would undoubtedly cause bigger problems than the original solution. Multiple inheritance from a class FLYING_THING would not help much. So far, only a minority of Eiffel users have admittedly reported ostrich-oriented programming as their major area of technical interest. But the need to deal with imperfect inheritance structures seems universal. Of course, we should strive to make these structures as complete and regular as possible. But we must also accept that unexpected special cases and exceptions may always occur. When they do and the programmer is only performing safe manipulations, the programming environment should help him, not put undue restrictions in his way. 4.3 Rationale for the redefinition rule The analysis of the redefinition rule is similar to the preceding discussion of the export rule. It is in fact hard to see what convention other than the one used in Eiffel can have any practical value. Consider classes HEIR and PARENT as above, and add HEIR_LIST and PARENT_LIST representing lists of objects of these respective types. Of course, the normal Eiffel method is to use genericity and declare these classes as LIST [HEIR] and LIST [PARENT]. But the use of genericity does not affect this discussion. Clearly, if every instance of HEIR ``is-an'' instance of PARENT, a list of HEIR objects also ``is-a'' list of PARENT objects. This and other reasons suggest that HEIR_LIST should inherit from PARENT_LIST. The conformance rules indeed ensure this if genericity is used. Assume that PARENT_LIST contains a procedure insert with an argument of type PARENT. Clearly, we only want to insert HEIR objects into an HEIR_LIST. So insert should be redefined in HEIR_LIST so as to take an argument of type HEIR. This satisfies the Eiffel rule for redefining routine arguments - the covariant policy. (In practical Eiffel programming, no explicit redefinition will be used; the effect is achieved more elegantly by a like something declaration, also known as declaration by association.) Interestingly, denotational models for inheritance (see [2] or the brief presentation in [6]) prescribe the reverse, ``contravariant'' rule: arguments can only be redefined to ancestor types of the original. This is apparently [3] the rule implemented in Trellis-Owl. Examples such as the above, of which there are thousands in practical Eiffel applications, make it very hard to imagine how significant object-oriented software can be written in a typed language without a covariant policy. Many of these examples use declaration by association, which is only a syntactical abbreviation, but in practice an essential one; its very availability for routine arguments is only possible because of the covariant rule. Pronouncements that the contravariant rule is ``the correct policy'', based on the revealed truths of denotational semantics, are surprising. (When the facts revolt, send in the lambda troops!). To be sure, the simplicity of mathematical models is an important guideline for assessing programming language decisions. Yet a model that conflicts with practical needs of software development loses its usefulness. A model is only an operational description of some reality. If the two do not match, the scientific method suggests that we should change the model, not the reality. The problem with the covariant rule, of course, is that it opens the possibility of type failures of the kind called /2/ above, which readily transposes to our latest example: /4/ pl: PARENT_LIST; hl: HEIR_LIST; p: PARENT; ... hl.Create; pl := hl; pl.insert (p) The answer to such a case is in line with the result of the discussion on the export-inheritance rule: put the burden on the compiler, not the compiler. Any occurrence of the last two above instructions in an Eiffel system should be detected by the checker; once again, their mere coexistence, without any consideration of whether the two can be part of the same control flow path, is sufficient cause for rejection. No flow analysis should be imposed on the checker. The next section specifies the type rules in light of the preceding discussion. The following one will outline the method to be followed by a checker to enforce these rules at reasonable cost. 5 THE TYPE RULE The type rule will be introduced under a number of simplifying assumptions, meant to keep the discussion clear. 5.1 Simplifications An Eiffel type will be taken to be defined by a class. This includes in fact two simplifications: + ``Expanded types'', which in particular include the basic types INTEGER, REAL etc., are not covered. These, however, are not involved in polymorphism, and hence do not raise any of the problems discussed above. + Generically parameterized types are also not covered. Genericity, essential in practical uses of Eiffel, does not fundamentally affect the current discussion. A consequence of this simplification is that ``B conforms to A'' is the same relation as ``B is a descendant of A''. For the purpose of this discussion, Eiffel may be viewed as having only two primitives: assignment and feature application. An assignment is of the form x := y and is a reference assignment. The left-hand side is an entity; the right-hand side is an expression. A feature application is either ``remote'' or ``local'', corresponding to the two forms x.f (a, b, ...) f (a, b, ...) where feature f may be an attribute or a routine. All feature applications will be considered to be remote applications of routines with exactly one argument, of the form: x.r (a) meaning ``Apply routine r to the object associated with x, if any, with the given arguments''. This simplification does not entail any loss of generality: + For local feature applications, we can consider that x is Current, the predefined entity representing the current object. + A routine with no argument may always be rewritten as having one argument, not used in the body. + For a feature f which is an attribute, we can write an associated function r with one argument (not used), returning the value of the attribute, and replace all applications of f by applications of r. + For a routine with more than one argument, the rules on a as given below are easily extended to rules applying to every formal argument and the corresponding actual arguments. The above does not consider ``multidot'' feature applications of the form a.b.c.d.... Although useful in practice, they can safely be ignored from a theoretical viewpoint since they can always be replaced by sequences of one-dot applications by using auxiliary variables (x := a.b; y := x.c; etc.) As a further simplification, we assume that no renaming is used, so that a feature defined in a class has the same name in all descendant classes, including those where it is redefined. This entails no loss of generality since renaming is a purely syntactic facility, albeit a very important one in practice. The only case for which renaming is indispensable is removing name clashes in multiple inheritance; for the purpose of this discussion we can assume that the original classes are rewritten so as to avoid any such class. In the same spirit we assume that when a routine is redefined the name of its formal argument (whose type may be redefined according to the covariant rule) does not change. 5.2 The goal of typing The preceding simplifications make it possible to express the goal of Eiffel typing in a complete yet simple way/ _________________________________________________ Type safety constraint: An Eiffel system is said to be type-safe if for any routine application x.r (a), and for any dynamic types TX and TA that x and a may take on during the execution of the system, TX includes and exports a routine corresponding to r, with a formal argument declared of a type which is an ancestor of TA. _________________________________________________ A system satisfying this constraint cannot suffer type failures at run time. It can still, however, suffer other failures, most notably by attempting to apply a routine r on a reference x that happens to be void. But this, as the division by zero case discussed at the beginning of this article, is not within the scope of typing strategies. Clearly, the contravariant rule, combined with either of policies 1 and 2 for export and inheritance, guarantees the type safety constraint. We must now see how to ensure it with the more liberal rules: policy 3 and the covariant rule. 5.3 The type rule The fundamental type rule will address the preceding requirements; it replaces (by strengthening it) the first rule of section 3.2. The rule uses the set Aliases (x) which, for any entity x in a system, contains all entities to which x may become aliased through assignment or routine call. A precise definition of this set will be given below. The type rule is the following: _________________________________________________ Type rule: An Eiffel system is type-correct if and only if the following two conditions are satisfied for any routine application x.r (z): + For every y in Aliases (x), S [y] exports r. + For every y in Aliases (x) and every t in Aliases (z), S [t] conforms to the type of the formal argument of r in S [y]. _________________________________________________ Pending a proper definition of Aliases, it is clear that this rule will satisfy the above type constraint. 5.4 Aliasing It remains to define Aliases (x) precisely. A more correct notation would be Aliases [S] (x) denoting the possible aliases of x with respect to a given system (set of classes) S. In what follows S will be considered to be fixed and the subscript will be dropped. Repeating the definition of a few basic concepts will be useful. + An entity is a name declared in a class, representing a reference which may be assigned values at run-time. Formally, then, an entity of name x appearing in class C is defined by the pair . For simplicity, entities will in fact be designated below given by their entity names only, but we must be careful to make it clear, for every x, what class C it belongs to. C will be called the class of x + Any entity x is declared of a certain type, called the static type of x and written T [x]. The declaration may appear in the class of the entity or, for an inherited entity, in an ancestor. + At any time during execution, the type of the object associated with a non-void entity is called the dynamic type of the entity and written D [x]. The second basic type rule (section 3.2) guarantees that the dynamic type conforms to the static type. + The definition of entities includes the predefined entity Result, denoting the result of a function. To resolve any ambiguity, the function name will be used in this case as name for the entity. Aliases is introduced through two binary relations. First entity y is said to be assignable to entity x if and only if any of the following assignments appears in the system: A.1 + x := y A.2 + x := b.y (t) for any b and t. In the second case, the relation holds not only for the entity y declared in S [b] but also to the corresponding entities in all the descendants of this class. Next, y is said to be bindable to x if and only if one of the following calls appears in S: B.1 + a.r (y) B.2 + a.r (b.y(t)) In both cases the relation holds whenever x is the formal argument for r in any descendant of S [a]; in the second case the relation extends to all y in any descendant of class S [b]. We say that y is a direct alias for x if y is assignable to x or bindable to x. Aliases (x) may now be defined by transitive reflexive closure: for any entity x, Aliases (x) is the set containing x itself and all entities y such that, for some z, y is a direct alias for z and (recursively) z belongs to Aliases (x). The above definitions consider all assignments and routine calls present in the system regardless of whether they may or may not be executed in actual runs of the system. So no flow analysis will be needed to enforce the type rule; as announced in 4.1, this will mean a pessimistic policy, although a less pessimistic one than policies 1 and 2. (The inclusion of all descendants of S [a] and S [b] in the above rules is also pessimistic; the aim here was to keep the definitions simple at no significant loss of useful systems. The interested reader may wish to examine how these conditions can be relaxed.) 6 IMPLEMENTING THE RULE [This section is only relevant for readers who are interested in the details of the incremental verification mechanism. Others are invited to proceed to the last section.] As introduced so far, the computation of Aliases (x) for every entity of a system does not take into account the order of compilation. As discussed in section 2.4, an essential requirement is the ability for the automatic incremental compilation mechanism to check a new class without re-checking the classes on which it depends - its suppliers and ancestors - if they have already been checked. Although the Eiffel incremental recompilation algorithm is not in the public domain, we may outline the strategy here. The first observation is that case B.2, which seems the most formidable one, can safely be ignored. By conceptually introducing a new entity z, we can rewrite the corresponding call as z := b.y (t); a.r (z) making B.2 a combination of A.2 and B.1. The incremental compilation requirement precludes the straightforward implementation of type checking, whereby we would compute Aliases (x) for every entity x, and then examine every feature call x.f (z) to see if it satisfies the type rule. True, this is appropriate for case A.2: whenever this case yields a new direct alias y for x, then the class of x is a client of the class of y, so that the set Aliases (x) may be updated in an order compatible with the compilation order. But this does not work for case B.1, where it is in fact the class of y which is a client of the class of x. (In case A.1 x and y belong to the same class.) As a consequence we must adopt a mixed strategy; the sets to be examined must be computable and adaptable in an order compatible with the dependency relation (and hence the compilation order). For every entity x, these sets will be: + Remote_aliases (x), the set of y for which A.2 holds; for convenience, this set also contains x. + Required_exports (x), the set of routines r which must be exported by the class of x because the system contains a call z.f (t) for some z such that x is in Aliases (z). + Required_types (x), the set of types C to which the S [x] must conform because the system contains a call z.f (t), where f requires a formal argument of type C, for some z such that x is in Aliases (z). The strategy to follow conceptually involves four steps for each new class. Step 1 initializes the above sets for each entity x of the class: the first set is initialized to the set containing just x itself; the second, to the set of f such that x.f (...) appears in the class; the last, to the types of the corresponding arguments. Step 2 propagates aliasing information to descendants. Whenever a new class HEIR is defined as heir to an existing one PARENT, step 2 performs the following for every entity x of HEIR (where x' is the corresponding entity in PARENT): + Remote_aliases (x) := Remote_aliases (x) U Remote_aliases (x') + Required_exports (x) := Required_exports (x) U Required_exports (x') + Required_types (x) := Required_types (x) ^ Required_types (x') [Nroff note: ^ means intersection, U means union]. This step implements the rule given in the previous section for both the ``assignable'' and ``bindable'' relations: any alias of an entity of class PARENT is considered to be also an alias of the corresponding entities in descendants of PARENT. For each new class, step 3 will perform the incremental computation of the three above sets and step 4 will verify that these sets satisfy the type rule. As will be seen below, these two steps may be performed simultaneously on each class. Step 3, when encountering any of the first three types of potential aliasing introduced above, must update the sets as follows: A.1 + Required_exports (y) := Required_exports (y) U Required_exports (x) Required_types (y) := Required_types (x) ^ Required_types (x) A.2 + Remote_aliases (x) := Remote_aliases (x) U Remote_aliases (y) B.1 + Required_exports (y) := Required_exports (y) U Required_exports (x) Required_types (y) := Required_types (y) ^ Required_types (x) In each of these cases the updating has been chosen so that it only affects some sets A (x) for an entity x in the new class, not in its (possibly old) suppliers. Using the above updates, the given sets are computed incrementally in an order which is compatible with inter- class dependencies, so that the computation may be integrated with the automatic compiling mechanism. Once this has been done, step 4 establishes the type rule for every new class C by checking the following two properties for every entity x in C: P1 + Every routine r in Required_exports (y), for every y in Remote_aliases (x), is exported by C. P2 + S [a] belongs to Required_types (y) for all y in Remote_aliases (x). In practice, step 4 may be performed at the same time as step 3 on each class C. Property P1 may be verified incrementally by checking in cases A.1 and B.1 that r belongs to Required_exports (y). P2 is verified incrementally by checking in cases A.1 and B.1 that S [A] belongs to Required_types (y). This incremental checking assumes that some initial verification has been integrated with steps 1 and 2. The details are easily filled. It is interesting to note that this initialization of the complete checking process is precisely the set of verifications performed by the current Eiffel compiler, reflecting the first and second rules described in section 3.2. As this discussion as shown, the full checking strategy is an extension to this partial approach. 7 ASSESSMENT To conclude, it is useful to examine a few possible objections to the rules and enforcement strategy described above. A first possible objection is that the algorithm sketched in the previous section is too difficult to integrate with the current Eiffel compiler. Of course, the only way to refute this objection would be to present the implementation, which is still some time away. The objection can only be made, however, by someone who does not realize the sophistication of some of the tasks already performed by the current Eiffel compiler (for example the implementation of repeated inheritance). A related objection addresses the cost of the new checking, especially in space. The precise impact needs to be assessed more carefully, but I believe the checking can reasonably be integrated within the normal compiling mechanism. If not, the mechanism would still be available as a compiler option a` la Lint, to be applied to systems at validation time. Perhaps the most serious objection has to do with the relative complexity of the mechanism described in the preceding section. But this mechanism is of no interest to normal users of the language; only implementors (and others doubtful of the soundness and enforceability oe the type rules) need understand it. Eiffel programmers will need to learn the type rule of section 5.3. This rule is only slightly more complex than the old type rule (first rule of section 3.2), which implies it; the advantage of the new rule should be clear to programmers reading a simplified form of the ``rationale'' section of this article (4). An attractive property of the incremental strategy described in the last section is that it appears to make it possible for the checker to produce clear and precise error messages, of the form ``In line m, feature f is applied to x; however, because of the assignment on line n, x might dynamically be of type D, which does not export f.'' If, as seems to be the case, the Eiffel compiler can reach this level of sophistication, then we will have achieved our goal. The purpose of a typed language is the same as the purpose of the programming environment of which it is a part: to help programmers, not bother them. Restrictions should boost programmer productivity by enabling an automatic checker to catch errors that would be difficult for a human being to detect. The liberal typing policy that has been integrated in Eiffel (``policy 3'') was designed to make programmers' life easier. The type failures to which it may lead are results of abnormal situations. Detecting such situations statically is a tricky and tedious business; as any such business, it should be handled by computers, not by humans. Acknowledgments I am deeply indebted to all the people who contributed to the type debate, including those with whose conclusions I sharply disagree, for forcing me to clarify the matter of types in Eiffel. References 1. Pierre America, Review of ``Object-Oriented Software Construction'', Science of Computer Programming, 1989, to appear (or having appeared already?) 2. Luca Cardelli, "A Semantics of Multiple Inheritance," in Semantics of Data Types (Eds. Gilles Kahn, David B. McQueen and Gordon Plotkin), Lecture Notes in Computer Science 173, pp. 51-67, Springer-Verlag, New York, 1984. 3. William Cook, "A Proposal for Making Eiffel Type-Safe," ECOOP Conference, 1989. 4. Philippe Elinck, "De la Conception-Programmation par Objets," Me'moire de Licence en Informatique (BS Thesis), Universite' Libre de Bruxelles, 1988. 5. Bertrand Meyer, Object-Oriented Software Construction, Prentice-Hall, 1988. 6. Bertrand Meyer, An Introduction to the Theory of Programming Languages, Prentice-Hall, 1989. To appear. 7. Bertrand Meyer, "Eiffel: An Introduction," Technical Report TR-EI-3/GI, Interactive Software Engineering Inc., 1986 (Last revision: 1988). 8. Craig Schaffert, Topher Cooper, Bruce Bullis, Mike Kilian, and Carrie Wilpolt, "An Introduction to Trellis-Owl," in OOPSLA '86 Conference Proceedings, Portland (Oreg.), Sept. 29-Oct. 2, 1986, pp. 9-16, 1986. (Published as SIGPLAN Notices, 21, 11, Nov. 1986.) -- -- Bertrand Meyer bertrand@eiffel.com