NICE-ESG-Libs Digest Sat, 30 Jul 94 Volume 1 : Issue 114 Today's Topics: Gustave Kernel (1/9): Introduction and Rationale Gustave Kernel (2/9): Proposed Conformance Rules ---------------------------------------------------------------------- NICE Eiffel Standards Group -- Library Committee Mailing List To post to list: NICE-ESG-Libs@atlanta.twr.com To send mail to the Chairman of the committee: NICE-ESG-Libs-chair@atlanta.twr.com Administrative matters (sign up, unsubscribe, mail problems, etc): NICE-ESG-Libs-request@atlanta.twr.com ---------------------------------------------------------------------- Date: Sat, 30 Jul 94 18:15:21 EDT >From: gustave Subject: Gustave Kernel (1/9): Introduction and Rationale The Gustave Kernel A proposal submitted to The Nonprofit International Consortium for Eiffel (NICE) by The Gustave Project sponsored by Tower Technology Corporation SwisSoft Everything Eiffel July 30, 1994 Introduction ------------ Gustave is a complete self-contained Eiffel kernel that is designed to provide a well defined set of base classes upon which portable Eiffel programs can be written. The Gustave kernel is not simply a snapshot of a particular vendor's existing classes, but is a critical synthesis of all existing kernels as well as some unifying additions which make Gustave a coherent, complete and precise base library. Particular attention has been paid to carefully specify the contract (pre- and post-conditions) of each feature in the kernel. The name "Gustave" for this kernel is, of course, the first name of the creator of the Eiffel Tower, Gustave Eiffel. A companion document, "Conformance Criteria", details the compatibility rules which we think are necessary for a truly interoperable kernel library specification. Roadmap ------- The proposal is being submitted in several parts in order to make each part digestable by the vageries of electronic mail. The parts consist of: Part 1: Introduction and Rationale This section discusses the overall design philisophy of Gustave. Part 2: Proposed Conformance Criteria Outlines a set of rules that can be used to judge whether a given kernel adhears to the kernel library standard. It suggests a set of mechanisms to cope with the inevitable need for a vendor to add non-standard features to access peculiarities of its runtime model. Parts 3 - 7: Class Rationales Textual descriptions of the design principles and tradeoffs made for each subkernel (Universal classes, ARRAY and STRING, comparable and numeric, basic types). Parts 8 - 9: Shorts These parts contain short forms of the classes comprising Gustave. Design Philosophy ------ ---------- Impact on Existing Kernels (vendor perspective) ------ -- -------- ------- ------ ----------- The Gustave kernel is the result of a great deal of negotiation and compromise between three of the four existing vendors. It has much in common with all existing vendor kernels, yet is different from each existing kernel. No single vendor will gain a unfair advantage from the adoption of Gustave. Although the implementation of the Gustave Standard Kernel will require work from all vendors, we believe that the resulting benefit to Eiffel (and the corresponding growth in the Eiffel library components market) will return a benefit to all. Most importantly, Gustave represents a complete kernel that the members of the Gustave Project feel can be supported without extension and thus has a great potential for providing greatly enhanced interoperability between diverse Eiffel implementations. Impact on Existing Kernels (programmer perspective) ------ -- -------- ------- ---------- ----------- At first glance, the Gustave kernel may appear to be very different from the kernel presented in ETL/2. This is not really the case. The vast majority of features in Gustave are either identical, or have been altered in only very slight (but we think important) ways. This often is simply a strengthening of the feature's contract, a change in the type of a formal argument, etc. None of these changes were made arbitrarily, but instead are the result of careful analysis as is pointed out in each class's supporting rationale. The most noticable differences are found in the ARRAY and STRING classes which have been streamlined and whose feature sets now closely resemble one another. Time Scales ---- ------ As far as adopting the Gustave kernel and having the Eiffel community receive the benefits of interoperability, the crutial time aspect will be the NICE committee's approval process (the implementation of the kernel by each vendor should be straightforward and relatively quick). We stand ready to assist the committee with understanding the prospoal and to provide additional insight into the various design decisions made in its development. Language Supporting Classes and Features -------- ---------- ------- --- -------- A number of features provided by the kernel library are intimately tied to the definition of the Eiffel language itself. For example, the reattachment semantics of expanded types involve the `standard_clone' and `standard_copy' features of class GENERAL. The Gustave `core' is completely compatible with the language requirements of ETL/2. A number of other features of the ETL/2 kernel library, such as STRING's `remove_all_occurrences' function, do not have special language status and were considered subject to change, revision, or even elimination. As minimal as possible, but no more -- ------- -- -------- --- -- ---- To paraphrase Albert Einstein, we have strived to make the Gustave kernel as minimal as possible, but no more. If the standard kernel is too minimal, then critical functionality will remain vendor specific and Eiffel systems using that functionality will not benefit from the standardization. On the other hand, we must resist the temptation to make Gustave a superset of existing practice since that can lead to baroque features and inconsistent naming. The standard classes are complete enough so that non-trivial Eiffel programs can be written without resorting to vendor-specific kernel extensions. Make vendor-specific extensions obvious to the programmer ---- ------ -------- ---------- ------- -- --- ---------- Should a vendor choose to extend the standard kernel, he is encouraged to do so by implementing descendant classes of standard classes (or implementing unrelated classes) rather than by adding vendor specific features to the standard class. Adding vendor-specific features or ancestors to `standard' classes make it less clear to the programmer whether he is calling a standard feature or an extension. See the companion document, "Conformance Criteria" for a list of suggested rules for judging whether a kernel conforms to the standard). Ancestry is Important -------- -- --------- Inheritance is significant. The fact that, for example, STRING is derived from COMPARABLE and HASHABLE has profound meaning. Similarly, feature adaptation is significant in that it affects whether descendent classes need to rename, select, or otherwise adapt features inherited from standard classes. The Standard must define precisely where features have their origin, where they are redefined, and where they are renamed. Standard classes must not inherit from vendor-specific classes outside of the kernel - to do so alters their place in the type hierarchy and thus fundamentally changes them between implementations. Because of these observations, the short forms given in this proposal include precise `inherit' clauses in the header comments for each class, including any necessary feature adaptation. Classes are More than Modules ------- --- ---- ---- ------- Classes like COMPARABLE and NUMERIC model specific and well defined mathematical concepts. Their features, therefore, are defined in a way compatible with those concepts. The Gustave NUMERIC class closely implements the mathematical notion of rings. Some existing NUMERIC classes (e.g, the one presented in ETL/2) do not. This explains some minor (but important) differences between the definitions of such classes. For example, one could not correctly implement a square matrix as a descendent of ETL's NUMERIC since raising a matrix to a real-numbered exponent is nonsensical. In the Gustave NUMERIC, the power operator is defined to take an integral exponent, which is compatible with square matrices and all other conceivable heirs of NUMERIC (complex numbers, polynomials, etc.). For more details, see the detailed discussion of the "Mathematical Classes" below. Assertions should be strong ---------- ------ -- ------ Great care has been made to make all preconditions as strong as possible. Sometimes this is little more than asserting that routine arguments are not Void. This is not as trivial as it may appear: since preconditions cannot be strengthened, an empty precondition (which is conceptually `true') effectively precludes any meaningful precondition on a routine. When it is possible to define the semantics of a class via its pre- and postconditions, we do so. This serves to keep descendant class programmers honest and honor the precise semantics of the feature - not just its superficial meaning. Sometimes this results in computationally complex assertions that might be too expensive to evaluate in practice (see the postcondition for infix "^" in NUMERIC) or which might not succeed due to system limitations (e.g. floating point precision problems may cause "a-b" to evaluate to a small, but non-zero value, so an assertion that says "(a-b)=zero" might fail for some representations). In these cases, we recognize that an implementation may need "comment out" such assertions. like Current vs. NUMERIC ---- ------- -- ------- While the numeric subkernel is much more rigorously defined than the one in ETL/2, from the user's point of view it is very similar. The most striking difference may be the use of "like Current" instead of NUMERIC in the signatures of the class NUMERIC. This is necessary in order to promote the use of foundation classes like NUMERIC as useful generic constraints. The use of "like Current" is normally used in preference to a hard classname. The reason for this is simple. Consider a generic class that needs to do some arithmetic on its elements, but wants to be generic enough to allow instantiation with INTEGER, REAL or DOUBLE. It might constrain its generic parameter to NUMERIC: class EXAMPLE [T -> NUMERIC] ... and then some feature may attempt to compute some values on the generic type: compute (x, y : T) : T do Result := x + y; end If "+" is defined, as it is in ETL/2, as: infix "+" (other : NUMERIC): NUMERIC then the EXAMPLE class is invalid since the expression `x+y' is of type NUMERIC and that does not conform to Result (which is of formal type T) because of the validity rule VNCF. By changing the signature to infix "+" (other : like Current): like Current the EXAMPLE class is valid, and NUMERIC becomes a useful generic constraint. Feature Names ------- ----- An attempt has been made to choose orthogonal names for related features. This sometimes conflicts with existing practice (for example, GENERAL's `out' has been renamed `to_string' for consistency with other type conversion features). Such renaming has precedent in Eiffel library development. Dr. Meyer published a paper ("Lessons from the Design of the Eiffel Libraries", CACM, Sept. 1990) describing similar changes made to the ISE data structures library where specialized feature names such as `top' in the STACK class were replaced with names more consistent with the rest of the library (e.g., `item'). Fortunately, Eiffel provides a mechanism for coping with changes like this: the Obsolete clause. A vendor may choose to provide access to the feature via the old name and mark the old name `obsolete'. Open Issues ---- ------ The Gustave Project has deliberately left some issues undecided. These are primarily related to choosing common ancestors to factor common features from related classes. For example, the feature sets of STRING and ARRAY are extremely similar and would benefit from a common ancestor encapsulating the notion of sequence. Similarly BIT_REF shares the `item' and `put' features with ARRAY and STRING, which would ideally originate in a common ancestor (SEQUENCE, INDEXABLE?). Since such classes are currently relegated to vendor-specific data structures libraries, it seems prudent to defer choosing precise ancestory for these classes to the Committee as a whole. Format of the Short forms ------ -- --- ----- ----- The classes included in this proposal are not quite in the traditional short-flat format. This is because, for this standard, short-flat signatures are not sufficient to precisely define each class. In the class header comment, each class lists its inheritence clauses, complete with any feature adaptation. Each class provides complete feature signature (header comments, assertions, etc.) only for those features which it introduces or redefined. For convenience, a summary section lists a one-line summary of all the (non-universal) features of the flattened class. Inherited features are listed by class of origin to clarify where they came from. Features inherited from the universal classes (GENERAL, PLATFORM, ANY) but not redefined are not listed even in the summary section. Features which redefine inherited features display their flattened assertions (postconditions are concatenated; preconditions are or'd) instead of the "require else" or "ensure then" clauses that would be found in the class text. ================================================== Date: Sat, 30 Jul 94 18:15:22 EDT >From: gustave Subject: Gustave Kernel (2/9): Proposed Conformance Rules The Gustave Kernel Proposed Conformance Criteria Introduction ------------ In order for a standard kernel to truly promote interoperability between vendors, it must be complete, and stand alone without reliance on vendor-specific libraries. Ideally it will be complete enough so that extensions can be prohibited (or at least, as is discussed below, restricted). Standalone Kernel ---------- ------ In order to promote the highest level of interoperability, a kernel library must be completely self contained and not rely on classes from outside it. By its very definition, a kernel is a core upon which more complicated functionality is built. Therefore, the Gustave kernel defines a complete standalone set of classes to be implemented without access to vendor-specific libraries. Inheritance ----------- In a previous post, we've detailed why allowing kernel classes to inherit from non-standard, non-kernel classes compromises the goal of the Eiffel Standards Group: that of interoperability of libraries and programs between diverse Eiffel implementations. We will simply summarize the issues in this document. Inheritance is significant. The fact that, for example, STRING is derived from COMPARABLE and HASHABLE has profound meaning. For this reason, a conforming kernel must adhear to the inheritance described by the standard, with no extra or missing parents. Similarly, feature adaptation is significant in that it affects whether decsendant classes need to rename, select, or otherwise adapt features inherited from standard classes. The Standard must define precicely where features have their origin, where they are redefined, and where they are renamed. Because of these observations, the short forms given in this proposal include precise `inherit' clauses in the header comments for each class, including any necessary feature adaptation. Extensions ---------- Why not allow vendor-specific extensions? If vendor A provides a version of a class that is a functional superset of the standard one, ought that not be considered conforming? The primary problem is, of course, one of name-space pollution. If a programmer writes a library using vendor B's kernel, he may introduce a feature whose name clashes with one of vendor A's extensions, but will never know until someone attempts to compile his library with vendor A's compiler. Some Extensions are Unavoidable ---- ---------- --- ----------- Of course, deviation from the official set of features will be necessary in some cases (for example, secret features may be needed to access vendor-specific runtime features). Such routines, even if exported to {NONE} cannot be hidden from descendant classes, so a standard naming convention is important to prevent unexpected name clashes when deriving new classes from the kernel classes. We propose that any such extensions be clearly marked as vendor specific by requiring that their names be prefixed by a vendor-specific prefix (e.g., `tower_c_deep_equal', `ise_c_deep_equal', etc.). This reduces the chance that vendor-specific extensions will conflict with another vendor's implementation and also highlights to an end-user programmer that such a feature is inherently vendor-specific and therefore not portable. Extensions for Backwards Compatibility ---------- --- --------- ------------- A vendor may desire to continue to support features from its current kernel library that are no longer part of the Standard. This is allowed only if that feature is marked with an Obsolete clause. Such extra features are intended to be included only for a short time to ease the transition from an older kernel to the Standard. The Committee may wish to suggest a time frame when such `obsolete' features are no longer allowed in conforming kernels. Rules ----- A kernel is said to conform to this standard if it differs from it in only the following ways: * The order of features can be changed. Features can be grouped into different Feature_clauses than given in the standard (though the new feature clause's Clients lists must be identical to the corresponding Clients in the standard). * Indexing clauses can be added. * Class and feature header comments can be changed (though vendors are encouraged to include the given header comments at minimum). * Formal argument names may be changed. * If an extra feature is introduced, either: * Its name is prefixed with a vendor-specific prefix (e.g., `ise_c_clone'). Such a feature should not be generally exported. * Or, the feature is marked `obsolete' (as noted above, this allowance should be phased out by the committee at some point in the future). * Assertion tags can be renamed. Rationale: Allowing the above changes allows an implementation to improve the readability of the text, adapt comments or assertion tags to languages other than English, etc. None of the changes (except for the vendor-prefix and obsolete provisions for adding features) affect the semantics of the kernel. A conforming kernel cannot make any of the following changes: * Delete a required class. * Change the ancestry or feature adaptation of a class. * Add features (other than those allowed by the vendor-prefix or backwards-compatibility rules). * Added features must not be redefined within the kernel since this may later require third-party heirs to rename/select or redefine. Such feature adaptation will not be compatible with kernels not providing the extensions. * Delete features. * Change the export status of a feature. * Change the type of a feature or its arguments. * Change the contract (assertion tags can be changed, but the body of each assertion is not changable.) Rationale: Allowing any of the above changes could lead to incompatibilities with other kernel implementations. ================================================== End of NICE-ESG-Libs Digest ****************************** From tynor@atlanta.twr.com Sat Jul 30 16:16:02 1994 Date: Sat, 30 Jul 94 18:15:57 EDT Reply-To: NICE-ESG-Libs@atlanta.twr.com Subject: NICE-ESG-Libs Digest V1 #115 To: NICE-ESG-Libs-digest@atlanta.twr.com Content-Length: 40423 X-Lines: 1030 Status: RO NICE-ESG-Libs Digest Sat, 30 Jul 94 Volume 1 : Issue 115 Today's Topics: Gustave Kernel (3/9): Universal Classes Gustave Kernel (4/9): STRING and ARRAY Gustave Kernel (5/9): Basic Types and Reference Equivalents Gustave Kernel (6/9): Mathematical Classes Gustave Kernel (7/9): Other Classes ---------------------------------------------------------------------- NICE Eiffel Standards Group -- Library Committee Mailing List To post to list: NICE-ESG-Libs@atlanta.twr.com To send mail to the Chairman of the committee: NICE-ESG-Libs-chair@atlanta.twr.com Administrative matters (sign up, unsubscribe, mail problems, etc): NICE-ESG-Libs-request@atlanta.twr.com ---------------------------------------------------------------------- Date: Sat, 30 Jul 94 18:15:45 EDT >From: gustave Subject: Gustave Kernel (3/9): Universal Classes Universal Classes --------- ------- GENERAL, PLATFORM, ANY ------- -------- --- These three classes form the basis of the inheritance hierarchy described in ETL. ANY inherits from PLATFORM which inherits from GENERAL. This is the relationship described in ETL. Class GENERAL ----- ------- In Gustave, as in all other Eiffel kernels, GENERAL is the root of the Eiffel inheritance hierarchy. It is designed to be the location of all features which are common to all Eiffel classes. No attributes are part of GENERAL - only routines. A number of GENERAL's features are considered part of the Eiffel language definition. These features are those that are mentioned in ETL (and presumably in ETR) that are related to the semantics of the language itself, for example, `clone', `copy', etc. Gustave's philosophy is that these features are not subject to change without a corresponding change in the language definition. For the most part, Gustave's universal classes are similar to those described in ETL, Most differences occur in GENERAL where there have been several addition and deletions of non-language-dependent features. There are also a some differences in the pre and post conditions on routines found in ETL - primarily additions. Additions to ETL --------- -- --- is_deep_equal, standard_is_deep_equal, null_pointer, twin, standard_twin, deep_twin, standard_deep_twin, same_dynamic_type dynamic_type_id Deletions from ETL --------- ---- --- deep_copy, standard_deep_copy, last_out, print Renamed Features ------- -------- out as to_string, generator as dynamic_type, Reference values --------- ------ GENERAL contains the definition of two reference values. `Void' is the value used to indicate that an Eiffel reference refers to no object. Since there are no pointer constants in Eiffel, GENERAL also contains a feature `null_pointer' which performs the same function for external pointers. Primary features for equality cloning and copying ------- -------- --- -------- ------- --- ------- There are three primary pairs of features in GENERAL having to do with equality testing, copying, and cloning of objects. Each pair of features contains a frozen "standard" feature and a redefinable version. Where pre and post conditions allow, the features are defined as synonyms. The first two features of this type are `is_equal' and `standard_is_equal'. These features test whether their `other' parameter is field by field identical to Current according to ETL semantics. The second pair of features is `copy' and `standard_copy'. These features perform a field by field copy of the `other' argument into the Current object in accordance with ETL semantics. The third and final pair of features in this feature clause are `twin and `standard_twin'. These features are not present in ETL, but have been present in various incarnations of GENERAL in other kernels. `twin' and `standard_twin' create a new copy of Current. As such, they require the programmer to insure that they are not dispatched off of a Void reference. These were adopted into Gustave for several reasons: They are more primitive than the related features `clone' and `standard_clone' which clone their first argument rather than Current and perform an explicit check for Void. `clone' and `standard_clone' (which are also present in Gustave) can be implemented more efficiently in terms of `twin and `standard_twin' than vice versa. A number of people have noted that often a programmer knows that a particular variable is not Void without having to explicitly test. `twin' and `standard_twin' provide the programmer with the opportunity to avoid the test when it make sense. The `twin' / `clone' pair of features is analogous to the `is_equal' / `equal' pair of features. Since both `is_equal' and `equal' are provided, it makes sense to provide `twin' and `clone'. `twin', like `is_equal', can be dispatched off a formal generic and result in efficient cloning of an object even if the class is instantiated with a basic type (e.g., INTEGER). Given that both `i' and `j' are INTEGER's, to call `j:=clone(i)' would involve first promoting i to an INTEGER_REF (since the type of the argument is a reference type), then `demoting' the returned INTEGER_REF back to an INTEGER. A call to `j:=i.twin', on the other hand will probably be implemented as a simple copy. `twin' and `standard_twin' are more "object-oriented" than `clone' and `standard_clone' since we are telling objects to make copies of themselves rather than some unrelated third party. To see that this issue is more than cosmetic, consider the case of redefining cloning semantics in STRING. Suppose we do not provide `twin' and simply provide `clone'. We, therefore, must redefine `clone' in STRING. The hazard is that the redefinition relies on the fact that all calls that clone STRINGs must be dispatched off of STRINGs. If, in some other class, we write: Class FOO ... s1,s2: STRING; ... s2 := clone(s1); ... end the clone of s1 will not be done using the redefined clone in STRING. However, since twin "clones" Current it does not suffer from this problem. `twin' and `standard_twin' are not synonyms since their postconditions differ in the use of `is_equal' vs. `standard_is_equal'. It is intended that GENERAL's implementation of `twin' should make an explicit call to `copy' to initialize the object. This means that redefining the semantics of copy will redefine the semantics of twin. As a result, all that is needed to redefine the notion of object equality in descendents of GENERAL is a redefinition of `is_equal' and `copy'. All other "shallow" feature definitions follow from these two. (While Gustave's intent is for `twin' to be implemented using `copy', there seems no easy way to write postconditions that help to insure this.) See the section on `equal' and `clone' below further comments on this subject. Primary deep features ------- ---- -------- ETL does not define a "deep" version of `is_equal' but Gustave defines `is_deep_equal', for consistency with the "shallow" features described above. While `is_equal' tests whether two objects attributes are the same (using `='), `is_deep_equal' performs this task recursively for attributes that are object references. In other words, `is_deep_equal' test whether two object graphs, rooted at Current and `other' are isomorphic and the values of their corresponding non-reference attributes equal (via `='). The Gustave kernel does not include `deep_copy' since its semantics tend to be confusing and it seems to add little value over `deep_clone'. (`deep_clone' is described in the section on deep convenience functions below). The deep version of `twin' (`deep_twin') is also not in ETL but are introduced for the the same reasons as `twin'. They perform the task of making a recursive copy of Current. Note that if an object and its `twin' are `is_equal', an object and its `deep_twin' are `deep_equal'. Convenience features for equality and cloning ----------- -------- --- -------- --- ------- Gustave possesses several convenience features that are also present in ETL that have to do with equality testing and cloning. These features are implemented in terms of the "primary" features described above. For the most part, they remove the requirement that the programmer check for Void arguments before using the features. In addition, one feature, `standard_clone', plays a role in specifying the semantics of the language. The first convenience features are `clone' and `standard_clone'. These two features take a single argument and insure that it is not Void before using `twin' to create a copy of the argument. `clone' returns this copy. `clone' and `standard_clone' are not synonyms because of the use of `is_equal' and `standard_is_equal' in their respective postconditions. The second feature pair is `equal' and `standard_equal'. These two features take two arguments argument and test to see if the first argument "some" is `is_equal' to the second argument "other". `equal' and `standard_equal' are not synonyms because of the use of `is_equal' and `standard_is_equal' in their respective postconditions. At this point it is worth noting that Gustave's GENERAL is specified such that if the programmer desires to redefine the notion of equality for a class - as is the case in STRING, all that need be done is to redefine `is_equal' and `copy'. The convenience features listed in this section are all defined in (directly or indirectly) terms of `is_equal' and `copy'. Therefore redefining these two "primary" features effectively redefines the convenience features in a consistent manner. Deep convenience features ---- ----------- -------- Gustave provides "deep" analogs of `equal' and `clone'. The features, `deep_equal' and `standard_deep_equal', are implemented in terms of `is_deep_equal' and `standard_is_deep_equal'. Another pair of features, `deep_clone' and `standard_deep_clone' are implemented in terms of `deep_twin' and `standard_deep_twin'. These features add handling of Void values that the features that they are based on do not perform. Neither pair are synonyms since the classes in each pair differs in their use of `is_deep_equal' versus `standard_is_deep_equal' in post conditions. Conformance features ----------- -------- Gustave has two features to test for conformance between objects: `conforms_to' and `same_dynamic_type'. `conforms_to' test whether Current is a descendent of the argument `other'. The argument type of `other' must be GENERAL and not "like Current" since "like Current" prevents checking of some cases where conformance actually exists. For example: A / \ B C \ / D b: B c: C b.conforms_to(c) is not possible with "like Current", however, if b holds a D and c holds a C, dynamically speaking b does conform to c. `conforms_to' also takes into account actual generics in generic classes. It does not simply check whether the base classes conform. Therefore ARRAY[STRING] conforms to ARRAY[ANY], but ARRAY[STRING] does not conform to ARRAY[INTEGER]. This is as per VNCC (p 219) in ETL. Gustave adds `same_dynamic_type' which allows the programmer to check whether two objects were instantiated with exactly the same class type, (including generics). Object and class identification ------ --- ----- -------------- Several features are provided that provide string-based representations and "internal identifiers" for objects and classes: to_string : This feature returns a STRING that is a printable representation of Current. It is simply a renaming of the feature `out'. object_id : A frozen feature returning an integer which is guaranteed not to change during the objects lifetime. dynamic_type : This frozen feature returns a STRING that is a printable representation of Current's class. It includes all actual generics used to instantiate Current. dynamic_type_id : A frozen feature returning a INTEGER that is associated with the class of Current. The INTEGER is unique to the given class for the life of the program. Two different instantiations of a given generic class should have different dynamic_type_id's IO interface -- --------- The feature name `io' is reserved for use in conjunction with the Gustave I/O proposal, the subject of a separate document. Class PLATFORM ----- -------- Class PLATFORM exists in Gustave in essentially the same form as in ETL. The lone exception is the addition of `boolean_bits' for the sake of completeness. Class ANY ----- --- ANY contains no features - this is common to all current implementations. The idea behind a featureless ANY is that it allows the user to replace the traditional "ANY" with a custom version of ANY that introduces universal features unique to a given application. ================================================== Date: Sat, 30 Jul 94 18:15:47 EDT >From: gustave Subject: Gustave Kernel (4/9): STRING and ARRAY Overview of the Gustave ARRAY and STRING Classes -------- -- --- ------- ----- --- ------ ------- The Nature of Arrays and Strings in Eiffel --- ------ -- ------ --- ------- -- ------ In some languages, a string is simply an array of characters. In Eiffel, a STRING has much in common with an ARRAY, but a STRING is not simply an array of characters because: - An ARRAY has an arbitrary lower limit, whereas the lower limit for a STRING is always one. - An ARRAY is not comparable, nor is it hashable, whereas a STRING is both of these. - In many applications, the "neutral" element for a STRING is a space (rather than a null), whereas for an ARRAY the "neutral" element is the default value (VOID, 0, null, false etc). Nevertheless, STRING and ARRAY have much in common. The Gustave kernel makes the features for manipulating ARRAYs and STRINGs more complete, consistent and symmetric. This enhances the functionality whilst easing the learning curve. The question of whether ARRAY and STRING deserve a common ancestor is deliberately left open. A Consistent Feature Set for ARRAY and STRING - ---------- ------- --- --- ----- --- ------ First, we have a set of features which handle a single item ('put', 'item', 'insert', ...). Second, we have features which deal with item ranges (slices, intervals). There is a symmetry: if you can 'put' or 'insert' an item at a specific place you can also 'put' or 'insert' a whole range of items. one item range of items ======== ============== put put_range item item_range precede prepend extend append insert insert_range remove remove_range force force_range If you need to operate on a range of items, you need either features like 'item_range' and 'put_range' or you have to use a loop. However, these features can be implemented very efficiently (i.e. memcpy) - in fact much more efficiently than a loop can possibly be. `Move' is the feature used to implement most of the `range' features. Common Ancestry for ARRAY and STRING? ------ -------- --- ----- --- ------ Because both ARRAY and STRING comprise multiple elements, there is a certain commonality in their structure. It would be possible to extract some of that commonality into a common ancestor. For example, an ancestor class with a name like INDEXABLE might be the appropriate place for features such as `item', infix "@", `put', `valid_index', `count' and `empty'. However, we were unable to find a compelling advantage to doing this, and have not incorporated it into the Gustave Kernel. NICE may wish to consider this issue. In any case, the Gustave specification requires that any ancestor to a kernel class must also be standardized and included within the Gustave Kernel. Null Characters Allowed in Strings ---- ---------- ------- -- ------- Any character may appear in a Gustave STRING, including an ASCII NUL ('%/0/'). This will require care to be taken when Eiffel strings are interfaced to C routines. Naming Issues ------ ------ The Gustave kernel includes the feature `item_range' in both STRING and ARRAY. In STRING, this corresponds to the conventional term `substring'. We have chosen to use the common name `item_range' for ease of learning and ease of use, in the same way that modern STACK classes tend to use general terms rather than the stack-specific `push' and `pop'. We have observed that Eiffel newcomers (and even experienced Eiffel programmers) are often confused by the pairs (precede/prepend) and (extend/append), which don't fit nicely into the general naming scheme. We have retained the existing names, because we could not devise a better set. For example, the set (prepend/prepend_range) and (append/append_range) would clash with the existing use of the names `prepend' and `append'. The Feature `adapt' `Adapt' has been provided as a creation feature in both STRING and ARRAY, with a single argument of type STRING and ARRAY respectively. The purpose of `adapt' is to allow descendants of STRING and ARRAY to be initialized from manifest STRINGs and ARRAYs. This is a very straightforward way of making these manifest objects more useful. The Feature `make' for STRING --- ------- ----- --- ------ Eiffel strings are automatically resized, and a programmer need not be concerned with setting the size of a STRING. Yet often the maximum size of a string is known in advance, and a significant improvement in efficiency can be obtained if the runtime system is not continually resizing the string as characters are added. In the Gustave kernel, `make' takes an integer argument representing the expected maximum number of characters. This is nothing more than a hint to the compiler. A compiler may take this parameter into account when preallocating space for the STRING, or may ignore it completely. Alternatively, a programmer may always supply a parameter of zero, and depend upon the runtime system to automatically resize the STRING as necessary. Th parameter to `make' reflects an internal storage capacity, not the length of the string as returned by `count', which is always zero immediately after the execution of `make'. The parameter to `make' has no visible effect to the Eiffel programmer, except possibly in regard to performance. The Feature `move' --- ------- ----- This feature is fundamental to the implementation of other features (such as insert and remove), and is provided in a simple form. In particular, it does not re-initialize any items that are contained within the source range but not the destination range. If required, an "initializing" `move' can easily be built from the non-ititializing one, whereas the reverse would not be possible. If the destination range "falls off" the end of the string or array, no resizing is performed, and the excess elements are lost. `force' and `force_range' in STRING ------ --- ----- ------ -- ------ These features initialize any intervening newly-created character positions to space (' ') rather than to Ascii Null ('%/0/'), as the latter would be unlikely to be useful in practical applications. infix `+' for STRING ----- - --- ------ Infix '+' is somewhat redundant because one can achieve the same effect with new := clone (s1) new.append (s2) but new := s1 + s2 is both less verbose and more expressive, and is included in the Gustave kernel. It's a binary "+", not a free operator, so it has that precedence. Since comparison operators are the only other operators applicable to strings, the binary "+" precedence ensures that "a" + "b" < "c" is treated as ("a" + "b") < "c" Implementation feature `area' in ARRAY and STRING -------------- ------- ----- -- ----- --- ------ The proposed classes do not include an `area' feature. This is in recognition that the class SPECIAL which is typically used to implement it is highly compiler-specific and some implementations may not tolerate uncontrolled access or manipulation of the SPECIAL. Should a vendor wish to provide direct access to an `area'-like feature, we suggest that a feature with a vendor-specific prefix (e.g., `twr_area') can be introduced. Redefinition for Efficiency ------------ --- ---------- The feature `relative_to' is redefined in STRING for computational efficiency. The Gustave proposal requires that any such feature redefinition must be specifically provided for in the kernel specification. The NICE Committee may also wish to specifically provide for the redefintition of ">=" and "<=" in STRING for reasons of efficiency. Included and Excluded Features -------- --- -------- -------- The Gustave specification for ARRAY and STRING includes features which operate on structure of the ARRAY or STRING. We have tried to minimize the number of features which must examine the content of the ARRAY or STRING (such as operations to search within the string or array, or format the contents of a string). The only exceptions are operations inherited from COMPARABLE and HASHABLE, and the features `to_upper' and `to_lower'. If Gustave was to include content-examining features, there would be no way to know when to stop, since these are inherently application requirements, and belong in other classes. Summary ------- The Gustave Kernel specifies ARRAY and STRING classes that are powerful, usable, elegant and efficient. Gustave's ARRAY and STRING provide a sound, convenient basis for the development of serious Eiffel applications. ================================================== Date: Sat, 30 Jul 94 18:15:50 EDT >From: gustave Subject: Gustave Kernel (5/9): Basic Types and Reference Equivalents Overview of the Gustave CHARACTER_REF and CHARACTER CLASSES -------- -- --- ------- --------- --- --- --------- ------- The Nature of Characters in Eiffel --- ------ -- ---------- -- ------ Characters are a basic type in Eiffel, with a default initialization value (the null character '%/0/'). They are comparable (although the order is not defined by the Gustave kernel specification). They are also hashable. Feature `make' ------- ----- The export status of 'make' must be changed to NONE in the expanded class. Reason: c := ('a').make ('b') cannot work - i.e. you cannot change the value of a character constant. Feature Adaptation in the (expanded) Basic Type Classes ------- ---------- -- --- -------- ----- ---- ------- The expanded classes inherit from the corresponding _REF classes and do not introduce new features or change the names or export status of inherited features (with the exception of `make'). However, they must redefine all those features which use 'like Current'. To explain why, look at the following feature from CHARACTER_REF: infix "<" (other : like Current) : BOOLEAN This must be redefined in CHARACTER as infix "<" (other : CHARACTER) : BOOLEAN The reason is that 'like Current' always denotes a reference type - even in an expanded class. This feature adaptation has not been shown in the accompanying "short" form. The Nature of `item' --- ------ -- ----- CHARACTER_REF needs a function 'item' without arguments and with type the non-ref version, i.e.: item : CHARACTER 'Item' cannot be an attribute since then the corresponding basic type would (by inheritance) have an attribute of its own type. This is illegal, since it would introduce an expanded client cycle. This means that every implementation must cheat here. Included and Excluded Features -------- --- -------- -------- CHARACTER_REF introduces three conversion features plus the character classification features. It would not be appropriate to include features like `to_upper' and `to_lower' unless features like `is_upper' and `is_lower' exist to give them meaning, therefore the set of classification features is included. Other Basic Classes ----- ----- ------- The other Basic type classes and their reference equivalents follow the same general rules as CHARACTER and CHARACTER_REF. All the numeric basic types (DOUBLE, REAL, INTEGER), inherit from COMPARABLE_NUMERIC which can serve as a convenient formal generic constraint for generic numeric programming libraries. Those basic types that have an integral representation (CHARACTER, INTEGER) are also heirs to HASHABLE and provide a `hash_value' based on their value. All the basic types provide conversion features for converting from one type to another, so one can easily convert a character to an integer (via CHARACTER's `to_integer') or an integer to a character (via INTEGER's `to_character'), and so on. DOUBLE and REAL share identical feature sets and provide some additional coversion features for controlling truncation behavior: `ceiling', `floor', `round', etc. ================================================== Date: Sat, 30 Jul 94 18:15:48 EDT >From: gustave Subject: Gustave Kernel (6/9): Mathematical Classes Rationale for the Mathematical Classes --------- --- --- ------------ ------- These are the classes that provide basic mathematical capabilities to Eiffel classes. These classes were the original focus of the Gustave Project as we began our efforts to add rigor to our respective kernel libraries. This help explains why they have evolved the most from what current Eiffel kernels currently contain. As we changed these classes we tried to balance three seperate but vital concerns: 1) mathematical correctness, notwithstanding the natural limits of digital computation; 2) utility, especially for the expression of higher mathematical constructs; 3) clarity, so that non-mathematicians can use and derive from these classes with ease. Background ---------- A number of operators are predefined in the Eiffel language. These include the comparison operators (e.g. "<", "<=") and the numeric operators (e.g. "+", "-", "*"). These operators don't come in isolation, of course, but are accompanied by the fundamental predefined types INTEGER, REAL, STRING, and so forth that they support. Each of these classes could theoretically independently introduce its own required mathematical operators, but this goes against the general design principle of factoring out commonalities. Besides, this effort at factoring can produce classes that are useful for independent purposes beyond supporting the core kernel classes. In designing these "factored" classes, one must first identify what the classes in question really have in common. Obviously then we start with common features. While this is clearly the starting point, an equally important question is whether there exists a common _concept_ that descendant classes might share. Otherwise one would end up with classes which are modules, but not true types. In other words, the classes might become merely a collection of 'features' without a deeper concept that unifies these features. The Mathematical Concepts --- ------------ -------- For the classes in question here, it is quite easy to find the commonalities and the proper abstractions since mathematical theory gives us the guidelines. While we use these principles to guide our design, we also must remember to strive to choose class and feature names that are meaningful for all. The set of integers and reals are both ordered rings. It turns out that factoring the concepts of "order" and "ring" into seperate Eiffel classes is easy and useful. They become COMPARABLE and NUMERIC in the Gustave Kernel. (Note that 'RING' and 'ORDER' are inappropriate classnames since the individual instances of INTEGER (for example) are neither rings nor orders. Rather, they have the property of 'numeric behaviour' and of being 'comparable'.) A quick examination shows that CHARACTER and STRING are additional candidates for inheriting from COMPARABLE. Also, if NUMERIC corrctly represents the concept of a ring, it can be used to introduce complex numbers, polynomials, square matrices, etc. In order to make the list of mathematical classes more complete, you will find PART_COMPARABLE (which correspond to the mathematical notion of partial orders) and ADDABLE (which correspong to abelian groups) in the Gustave Kernel. Partial orders are a generalization of "total orders" as defined in COMPARABLE. The difference being they don't require that two elements must always be comparable with each other. Abelian groups (i.e. the 'addable' behaviour) are introduced because some mathematical objects have a natural additive structure but cannot be given the structure of a ring in the same natural way. Examples of this include the elements of a vector space. Summary ------- The interfaces reflect the mathematical definitions we are trying to capture in a manner that is as close as possible given the definition of Eiffel. While we have to live with the fact that the distributive law for rings cannot be expressed in NUMERIC, it is pleasant that a full and accurate description of the properties of total orders can be captured in Eiffel (as is done via the class COMPARABLE). The mathematical classes present in the Gustave Kernel were designed by mathematicians. While this peculiar species tends to be accurate (sometimes to the point of boredom), we claim that maximum accuracy is certainly appropriate when designing classes that directly reflect basic mathematical concepts. Addendum: Notes concerning some specific classes and/or features. COMPARABLE ---------- In any order, partial or not, one has the following rules: (1) a > b if and only if b < a (2) a >= b if and only if b <= a In fact, in mathematics the operators '>' and '>=' are _defined_ in these terms. (You can also use '>' and '>=' as a starting point and define the others in terms of them.) Furthermore, we have the law of trichotomy: If 'a' and 'b' are mutually comparable (always true in a total order), then exactly one of the following statements is true: (a) a < b (b) a 'equals' b (c) b < a Of course, in mathematics 'equals' is replaced by '='. But that doesn't matter, because the law actually _defines_ 'equals' thusly: a 'equals' b if and only if not (a < b) and not (b < a) (in case of mutual comparability). This simple observation is the reason why '<' and '<=' are so closely related (as we see in their respective postconditions in PART_COMPARABLE) and why '<=' is completely defined in terms of '<' in class COMPARABLE: a <= b if and only if not (b < a) The degree of freedom Gustave gives for the definition of '<=' is zero in the class COMPARABLE. There is not much freedom for the definition in PART_COMPARABLE. This yields rigor and correctness. NUMERIC ------- The only reasonable concept which can serve as a model for this class is that of an associative ring with 1 /= 0. You will certainly not be surprised by the features of this class, but some of the assertions and signatures need explanation. The feature 'is_valid_divisor' is necessary, because a condition of the form 'not_zero' is not sufficient in all cases for the division operator (consider polynomials or matrices). The power operator takes as argument an integer - you may find this to be too restrictive, but considered mathematically it is the only reasonable choice. To wit, whenever you have multiplication, you can take the n-th power of an element ('n' being an integer >= 0). If the element happens to be invertible, then you can take arbitrary integer powers. However, raising an element to the 'x-th' power, where 'x' is not an integer doesn't make any sense in the general case. Since we intend for NUMERIC to be a general class, we introduce the argument as an INTEGER -- and would do so even if the feature were deferred. (It is _not_ deferred - in fact it can be implemented _very_ efficiently.) A `power' feature which takes a floating point exponent is included in REAL_REF and INTEGER_REF, so one has the best of both worlds. Finally, as covered in detail in the "general principles" section, NUMERIC and related classes define many of their features with arguments and return values of the type "like Current" in order to facilitate the use of these classes as generic constraints. ================================================== Date: Sat, 30 Jul 94 18:15:51 EDT >From: gustave Subject: Gustave Kernel (7/9): Other Classes Rationale for Runtime and OS Services Classes --------- --- ------- --- -- -------- ------- This section describes the Gustave design for the classes that provide access to services provided by the Eiffel run-time or by the operating system. THIS SECTION OF THE DOCUMENTATION FOR NICE MUST BE CONSIDERED AS TENTATIVE AT THIS TIME. IT IS INCLUDED TO PROVIDE INSIGHT TO THE LIBRARY COMMITTEE INTO SOME OF THE THINKING OF THE GUSTAVE PROJECT MEMBERS CONCERNING THESE CLASSES. THIS SECTION IS NOT FINAL. [ A non-technical note for NICE Library Committee mambers: The original plan for the Gustave Project was to complete the Gustave Kernel by late summer. The internal plan was to first concentrate on the classes that provide direct support for the Eiffel language. Only after this was accomplished would we go back and work on the classes that provide interfaces to runtime and OS services. The NICE deadline for kernel submissions has forced us to delay submitting final detailed class descriptions for the classes in this category. We are confident that we will have these class descriptions completed by the time that the Library Committee will need them for consideration. We will, of course, make them available as soon as possible. ] Runtime Interface Classes ------- --------- ------- MEMORY ------ As this class has been traditionally implemented, it serves two distinct purposes. First, it provides an interface to the garbage collector. Second, it defines the special feature `dispose' that, if redefined in a decendent class, is invoked for the purposes of freeing external resources after collection has occured for the instance. Combining these two purposes causes two problems: 1) MEMORY must be implemented with as few attributes as possible -- preferable zero -- as we do not wish to require attributes from this class to be placed into descendent classes just because they need to redefine `dispose'. (One released kernel library works around this problem by defining a seperate GC_INFO class rather than simply adding on to MEMORY. This approach deserves consideration.) 2) Finalization is hidden away at the end of a moderately obscure class. Many people who are new to Eiffel become concerned about how to deal with deallocation of external resources and don't stumble across `dispose'. Certainly we don't want to encourage people to use this capability inapropriately, but we shouldn't be obscure about this. 3) Finalization by the redefinition of an inherited feature is not specified by the Eiffel language definition. Other schemes to accomplish the same purpose are possible. Completely safe mechanisms may be possible. Because of these problems, the Gustave Project is considering a number of possible options. If we can't convince ourselves that an `asymptotic to perfection' solution is available, then we may settle for a new class called FINALIZATION (or DISPOSABLE) with a "special" feature `finalize' (or `dispose') in the same manner as the current scheme, but seperate from class MEMORY. EXCEPTIONS ---------- The Gustave Project strongly suggests that the capabilities that are typically defined in class EXCEPTIONS be standardized. This includes a core set of names for the various types of exceptions and signals. Like the class MEMORY, the Gustave Project notes that class EXCEPTIONS combines multiple distinct purposes into a single class. This indicates to us that this class may also be better off by being split into separate classes. The purposes we note are: 1) Defining constants that denote types of exceptions and signals. 2) Controlling how signals will be handled. 3) Defining a continuation feature (basically a signal handler) that will be invoked when designated types of signals occur. 4) Extracting information about exceptions that have occured. One proposal within Gustave includes the definition of a deferred class called SIGNAL_HANDLER or EXCEPTION_HANDLER with a single deferred feature called `handle' that can be effected by users and registered with the EXCEPTIONS class as the current handler. This replaces the current scheme whereby the class EXCEPTIONS itself must be specialized and a feature like `continue_action' must be redefined. (The current scheme seems problematic in the face of the possibility of seperate redefintion of `continue_action' in seperately derived classes. The semantics for determining which version of the feature is in force are not clearcut.) Interface to Operating System Services --------- -- --------- ------ -------- I/O, FILES and Related Classes - - ----- --- ------- ------- The Gustave Project strongly feels that I/O and file handling classes should be included in the Eiffel Standard Kernel. The complete Gustave I/O proposal is under development and will be submitted seperately at a later date. Here are some notes on the design of the I/O and related classes: ------------ The I/O and file handling capabilities included in the Gustave Kernel will be independent of the underlying operating system. Designing instantly portable classes is a significant challenge, but necessary for the success of any interoperable kernel library. ------------ It is suggested that the feature name `io' be reserved in class GENERAL for possible use in conjunction with the forthcoming I/O classes. ------------ In general, the Gustave Project thinks that I/O should be based on a transport-independent layer. ------------ Some thought has been given to the notion that I/O should be independent of, but easy to use in conjunction with, the notion of formatting. One notion is to explore formatting in terms of STRINGs -- i.e. a class like STRING_FORMATTER, STRING_PARSER and so forth -- rather than clutter I/O with the notion of formatted data. ------------ If we have the notion of a transport-independent I/O substrate, then it makes sense to consider defining a notion of serializing and unserializing Eiffel objects using an address space independent stream of bytes. This can utilize the I/O substrate in any of a variety of ways -- using pipes, files, sockets, etc. ------------ We note that the notion of interoperability in regards to sharing serialized objects as byte streams between Eiffel implementations is more of a compiler/runtime issue than a Library issue. A Standard Eiffel Library probably won't be able to guarantee such interoperation. Other Classes ----- ------- Gustave notes that other possible OS and runtime interfaces could be standardized, but no serious thought has been given to these yet. The likelihood is that they will not be included in the Gustave Kernel. Accessing Class and Instance Information --------- ----- --- -------- ----------- The classes provided by the three main Eiffel vendors for accessing class and instance information in a low-level manner are suprisingly consistent with each other -- despite having completely different class and feature names. Standardizing a common subset of this low-level interface as an optional adjunt to the Gustave Kernel would probably be straightforward and yield positive benefit to third party suppliers of Eiffel programming tools, database interface libraries and other places where a generalized interface with Eiffel instances and classes are required. ARGUMENTS, ENVIRONMENT --------- ----------- These classes are both useful and simple enough to be considered for standardization in order to improve interoperability. ================================================== End of NICE-ESG-Libs Digest ****************************** From tynor@atlanta.twr.com Sat Jul 30 16:26:49 1994 Date: Sat, 30 Jul 94 18:16:12 EDT Reply-To: NICE-ESG-Libs@atlanta.twr.com Subject: NICE-ESG-Libs Digest V1 #116 To: NICE-ESG-Libs-digest@atlanta.twr.com Content-Length: 87226 X-Lines: 2961 Status: RO NICE-ESG-Libs Digest Sat, 30 Jul 94 Volume 1 : Issue 116 Today's Topics: Gustave Kernel (8/9): Shorts (1/2) Gustave Kernel (9/9): Shorts (2/2) ---------------------------------------------------------------------- NICE Eiffel Standards Group -- Library Committee Mailing List To post to list: NICE-ESG-Libs@atlanta.twr.com To send mail to the Chairman of the committee: NICE-ESG-Libs-chair@atlanta.twr.com Administrative matters (sign up, unsubscribe, mail problems, etc): NICE-ESG-Libs-request@atlanta.twr.com ---------------------------------------------------------------------- Date: Sat, 30 Jul 94 18:16:05 EDT >From: gustave Subject: Gustave Kernel (8/9): Shorts (1/2) -- Universal features. -- -- All Eiffel classes inherit from `ANY', which inherits from `PLATFORM', -- itself an heir of `GENERAL'. -- -- Inheritance: -- -- none class interface GENERAL ancestors GENERAL feature summary {GENERAL} clone (other : GENERAL) : like other frozen conforms_to (other : GENERAL) : BOOLEAN copy (other : like Current) frozen deep_clone (some : GENERAL) : like some frozen deep_equal (some : GENERAL; other : like some) : BOOLEAN frozen deep_twin : like Current default_rescue frozen dynamic_type_id : INTEGER frozen dynamic_type_name : STRING equal (some : GENERAL; other : like some) : BOOLEAN frozen is_deep_equal (other : like Current) : BOOLEAN is_equal (other : like Current) : BOOLEAN frozen null_pointer : POINTER frozen object_id : INTEGER frozen same_dynamic_type (other : GENERAL) : BOOLEAN frozen standard_clone (other : GENERAL) : like other frozen standard_copy (other : like Current) frozen standard_equal (some : GENERAL; other : like some) : BOOLEAN frozen standard_is_equal (other : like Current) : BOOLEAN frozen standard_to_string : STRING frozen standard_twin : like Current to_string : STRING twin : like Current frozen void : NONE creation -- This class cannot be instantiated. feature specification {GENERAL} -- Void values frozen void : NONE -- Void reference. frozen null_pointer : POINTER -- Null pointer. feature specification {GENERAL} -- Equality, clone, copy. frozen standard_is_equal, is_equal (other : like Current) : BOOLEAN -- Is `other' field-by-field identical to `Current'? Compares only -- those fields that are in `Current' (which may have different names -- in `other'). require other_not_void : other /= void; copy (other : like Current) -- Copy every field in `Current' from the corresponding field `other'. require other_not_void : other /= void; ensure is_equal : is_equal (other); frozen standard_copy (other : like Current) -- Copy every field in `Current' from the corresponding field `other'. require other_not_void : other /= void; ensure is_equal : standard_is_equal (other); twin : like Current -- New object field-by-field identical to `Current'. ensure not_void : Result /= void; is_equal : Result.is_equal (Current); frozen standard_twin : like Current -- New object field-by-field identical to `Current' ensure not_void : Result /= void; is_equal : Result.standard_is_equal (Current); feature specification {GENERAL} -- Deep object graph equality and cloning frozen is_deep_equal (other : like Current) : BOOLEAN -- Are the object graphs rooted at `Current' -- and `other' isomorphic? ensure reflexive : is_equal (other) implies Result; symmetric : Result = other.is_deep_equal (Current); only_if_same_type : (not same_dynamic_type (other)) implies (not Result); frozen deep_twin : like Current -- A new object structure recursively duplicated from `Current'. ensure not_void : Result /= void; is_deep_equal : is_deep_equal (Result); feature specification {GENERAL} -- Convenience functions. clone (other : GENERAL) : like other -- Void if `other' is void; otherwise, a new object field-by-field -- identical to `other'. Uses `twin'. ensure is_equal : equal (Result, other); frozen standard_clone (other : GENERAL) : like other -- Void if `other' is void; otherwise, a new object field-by-field -- identical to `other'. Uses `standard_twin'. ensure is_equal : standard_equal (Result, other); equal (some : GENERAL; other : like some) : BOOLEAN -- Are `some' and `other' either both Void, or field-by-field -- identical one another? Uses `is_equal'. ensure is_equal : Result = (((some = void) and (other = void)) or else (((some /= void) and (other /= void)) and then some.is_equal (other))); frozen standard_equal (some : GENERAL; other : like some) : BOOLEAN -- Are `some' and `other' either both Void, or field-by-field -- identical one another? Uses `standard_is_equal'. ensure is_equal : Result = (((some = void) and (other = void)) or else (((some /= void) and (other /= void)) and then some.standard_is_equal (other))); feature specification {GENERAL} -- Deep convenience functions. frozen deep_equal (some : GENERAL; other : like some) : BOOLEAN -- Are `some' and `other' either both void, or recursively `equal' to -- one another? ensure is_deep_equal : (Result = ((some = void) and (other = void))) or else (((some /= void) and (other /= void)) and then some.is_deep_equal (other)); frozen deep_clone (some : GENERAL) : like some -- Void if `some' is void; otherwise, a new object structure -- recursively duplicated from `some'. ensure is_deep_equal : deep_equal (Result, some); feature specification {GENERAL} -- Conformance frozen conforms_to (other : GENERAL) : BOOLEAN -- Is dynamic type of `Current' a descendant of dynamic type of -- `other'? require other_not_void : other /= void; ensure reflexive : (Current = other) implies Result; frozen same_dynamic_type (other : GENERAL) : BOOLEAN -- Is dynamic type of `other' identical to the dynamic type of -- `Current'? require other_not_void : other /= void; ensure only_if_same_type : Result = (conforms_to (other) and other.conforms_to (Current)); feature specification {GENERAL} -- Default exception handling default_rescue -- Exception response for routines without a rescue clause. Default: -- do nothing. feature specification {GENERAL} -- Simple STRING representations of objects to_string, frozen standard_to_string : STRING -- New string containing a terse printable representation of -- `Current', field by field. ensure not_void : Result /= void; feature specification {GENERAL} -- Internal object properties frozen object_id : INTEGER -- A value associated with `Current' that is constant for the life of -- the object. The value is not necessarily unique and is not -- necessarily the same in another execution of the program. frozen dynamic_type_name : STRING -- Name of `Current's dynamic type; the class, including actual -- generic parameters, of which it is a direct instance. Every call -- to this function allocates a new result string. ensure not_void : Result /= void; frozen dynamic_type_id : INTEGER -- Like `object_id', a constant value associated with Current's -- generating class. See `dynamic_type_name'. end interface -- class GENERAL -- Platform-dependant features. -- -- Inheritance: -- GENERAL class interface PLATFORM ancestors PLATFORM GENERAL feature summary frozen bit_size : INTEGER frozen boolean_bits : INTEGER frozen character_bits : INTEGER frozen double_bits : INTEGER frozen integer_bits : INTEGER frozen maximum_character_code : INTEGER frozen pointer_bits : INTEGER frozen real_bits : INTEGER feature summary {GENERAL} clone (other : GENERAL) : like other frozen conforms_to (other : GENERAL) : BOOLEAN copy (other : like Current) frozen deep_clone (some : GENERAL) : like some frozen deep_equal (some : GENERAL; other : like some) : BOOLEAN frozen deep_twin : like Current default_rescue frozen dynamic_type_id : INTEGER frozen dynamic_type_name : STRING equal (some : GENERAL; other : like some) : BOOLEAN frozen is_deep_equal (other : like Current) : BOOLEAN is_equal (other : like Current) : BOOLEAN frozen null_pointer : POINTER frozen object_id : INTEGER frozen same_dynamic_type (other : GENERAL) : BOOLEAN frozen standard_clone (other : GENERAL) : like other frozen standard_copy (other : like Current) frozen standard_equal (some : GENERAL; other : like some) : BOOLEAN frozen standard_is_equal (other : like Current) : BOOLEAN frozen standard_to_string : STRING frozen standard_twin : like Current to_string : STRING twin : like Current frozen void : NONE creation -- This class cannot be instantiated. inherited features {GENERAL} -- From GENERAL: clone, conforms_to, copy, deep_clone, deep_equal, deep_twin, default_rescue, dynamic_type_id, dynamic_type_name, equal, is_deep_equal, is_equal, null_pointer, object_id, same_dynamic_type, standard_clone, standard_copy, standard_equal, standard_is_equal, standard_to_string, standard_twin, to_string, twin, void feature specification frozen character_bits : INTEGER is ??? -- Number of bits used to represent a CHARACTER entity frozen integer_bits : INTEGER is ??? -- Number of bits used to represent an INTEGER entity frozen real_bits : INTEGER is ??? -- Number of bits used to represent a REAL entity frozen double_bits : INTEGER is ??? -- Number of bits used to represent a DOUBLE entity frozen boolean_bits : INTEGER is ??? -- Number of bits used to represent a BOOLEAN entity frozen pointer_bits : INTEGER is ??? -- Number of bits used to represent an object reference frozen bit_size : INTEGER -- Number of bits used to represent `Current' frozen maximum_character_code : INTEGER is ??? -- Largest `code' for CHARACTER entities. end interface -- class PLATFORM -- Universal features. -- -- All Eiffel classes inherit from `ANY'. -- -- Inheritance: -- PLATFORM class interface ANY ancestors ANY PLATFORM GENERAL feature summary frozen bit_size : INTEGER frozen boolean_bits : INTEGER frozen character_bits : INTEGER frozen double_bits : INTEGER frozen integer_bits : INTEGER frozen maximum_character_code : INTEGER frozen pointer_bits : INTEGER frozen real_bits : INTEGER feature summary {GENERAL} clone (other : GENERAL) : like other frozen conforms_to (other : GENERAL) : BOOLEAN copy (other : like Current) frozen deep_clone (some : GENERAL) : like some frozen deep_equal (some : GENERAL; other : like some) : BOOLEAN frozen deep_twin : like Current default_rescue frozen dynamic_type_id : INTEGER frozen dynamic_type_name : STRING equal (some : GENERAL; other : like some) : BOOLEAN frozen is_deep_equal (other : like Current) : BOOLEAN is_equal (other : like Current) : BOOLEAN frozen null_pointer : POINTER frozen object_id : INTEGER frozen same_dynamic_type (other : GENERAL) : BOOLEAN frozen standard_clone (other : GENERAL) : like other frozen standard_copy (other : like Current) frozen standard_equal (some : GENERAL; other : like some) : BOOLEAN frozen standard_is_equal (other : like Current) : BOOLEAN frozen standard_to_string : STRING frozen standard_twin : like Current to_string : STRING twin : like Current frozen void : NONE inherited features -- From PLATFORM: bit_size, boolean_bits, character_bits, double_bits, integer_bits, maximum_character_code, pointer_bits, real_bits inherited features {GENERAL} -- From GENERAL: clone, conforms_to, copy, deep_clone, deep_equal, deep_twin, default_rescue, dynamic_type_id, dynamic_type_name, equal, is_deep_equal, is_equal, null_pointer, object_id, same_dynamic_type, standard_clone, standard_copy, standard_equal, standard_is_equal, standard_to_string, standard_twin, to_string, twin, void end interface -- class ANY -- Elements that may be compared in a partial order relation. If the elements -- being compared are not comparable with one another, these features return -- false. Note that partial equality is not necessarily the same as -- `is_equal', since `is_equal' is not necessarily tied to the notion of -- ordering. Therefore the partial ordering is defined in terms of the -- deferred features, `infix "<"' and `infix "<="'. -- -- Inheritance: -- -- none deferred class interface PART_COMPARABLE ancestors PART_COMPARABLE feature summary infix "<" (other : like Current) : BOOLEAN infix "<=" (other : like Current) : BOOLEAN infix ">" (other : like Current) : BOOLEAN infix ">=" (other : like Current) : BOOLEAN feature specification -- Deferred routines that determine the partial ordering. infix "<" (other : like Current) : BOOLEAN -- Is `Current' strictly less than `other'? require other_not_void : other /= void; deferred ensure consistent : Result implies (not (other <= Current)); not_reflexive : (Current = other) implies (not Result); infix "<=" (other : like Current) : BOOLEAN -- Is `Current' less than or equal to `other'? require other_not_void : other /= void; deferred ensure consistent : Result implies (not (other < Current)); reflexive : (Current = other) implies Result; feature specification -- Effective routines whose behavior are determined by the behavior of -- `infix "<"' and `infix "<="'. infix ">" (other : like Current) : BOOLEAN -- Is `Current' strictly greater than `other'? require other_not_void : other /= void; ensure other_is_less : Result = (other < Current); infix ">=" (other : like Current) : BOOLEAN -- Is `Current' greater than or equal to `other'? require other_not_void : other /= void; ensure other_less_or_equal : Result = (other <= Current); end interface -- class PART_COMPARABLE -- Elements that may be compared for a total order relation. Descendants need -- only define the behavior of `infix "<"'. -- -- Inheritance: -- PART_COMPARABLE -- redefine -- infix "<", -- infix "<=" -- end; deferred class interface COMPARABLE ancestors COMPARABLE PART_COMPARABLE feature summary infix "<" (other : like Current) : BOOLEAN infix "<=" (other : like Current) : BOOLEAN infix ">" (other : like Current) : BOOLEAN infix ">=" (other : like Current) : BOOLEAN max (other : like Current) : like Current min (other : like Current) : like Current relative_to (other : like Current) : INTEGER inherited features -- From PART_COMPARABLE: infix ">", infix ">=" feature specification -- Features from PART_COMPARABLE infix "<" (other : like Current) : BOOLEAN -- Is `Current' strictly less than `other'? -- This features determines the total ordering. -- -- Redefined from PART_COMPARABLE to strengthen the -- postcondition. require other_not_void : other /= void; deferred ensure other_not_less_or_equal : Result = (not (other <= Current)); consistent : Result implies (not (other <= Current)); not_reflexive : (Current = other) implies (not Result); infix "<=" (other : like Current) : BOOLEAN -- Is `Current' less than or equal to `other'? -- -- Effects the deferred feature from PART_COMPARABLE. require other_not_void : other /= void; ensure other_not_less : Result = (not (other < Current)); consistent : Result implies (not (other < Current)); reflexive : (Current = other) implies Result; feature specification -- Other useful features for comparable objects. relative_to (other : like Current) : INTEGER -- The relative position of `Current' to `other': -- `< 0' if `Current < other'; -- `0' if `Current = other'; -- `> 0' if `Current > other'. require other_not_void : other /= void; ensure negative_condition : (Result < 0) = (Current < other); zero_condition : (Result = 0) = (not ((Current < other) or (Current > other))); positive_condition : (Result > 0) = (Current > other); min (other : like Current) : like Current -- The smaller of `Current' and `other'; -- `Current' if thay are comparably equal. require other_not_void : other /= void; ensure not_void : Result /= void; current_if_less_equal : (Current <= other) implies (Result = Current); other_if_greater : (Current > other) implies (Result = other); max (other : like Current) : like Current -- The larger of `Current' and `other'; -- `other' if thay are comparably equal. require other_not_void : other /= void; ensure not_void : Result /= void; other_if_less_equal : (Current <= other) implies (Result = other); current_if_greater : (Current > other) implies (Result = Current); end interface -- class COMPARABLE -- ADDABLE represents the mathematical notion of a communitive group. -- -- Inheritance: -- -- none deferred class interface ADDABLE ancestors ADDABLE feature summary infix "+" (other : like Current) : like Current prefix "+" : like Current infix "-" (other : like Current) : like Current prefix "-" : like Current zero : like Current feature specification infix "+" (other : like Current) : like Current -- Sum of `Current' and `other' require other_not_void : other /= void; deferred ensure not_void : Result /= void; commutative : Result.is_equal (other + Current); infix "-" (other : like Current) : like Current -- Difference between `Current' and `other' require other_not_void : other /= void; ensure not_void : Result /= void; consistent : Result.is_equal (Current + (- other)); prefix "+" : like Current -- Unary addition applied to `Current' ensure not_void : Result /= void; does_nothing : Result.is_equal (Current); prefix "-" : like Current -- Unary subtraction applied to `Current' deferred ensure not_void : Result /= void; idempotent : (- Result).is_equal (Current); zero : like Current -- The neutral element of addition ensure not_void : Result /= void; consistent : Result.is_equal (Current - Current); end interface -- class ADDABLE -- NUMERIC represents the mathematical notion of a ring. -- -- Note that not all descendants are necessarily comparable (e.g. -- SQUARE_MATRIX). Comparable numeric classes should be constructed from -- COMPARABLE_NUMERIC. -- -- Inheritance: -- ADDABLE deferred class interface NUMERIC ancestors NUMERIC ADDABLE feature summary infix "*" (other : like Current) : like Current infix "+" (other : like Current) : like Current prefix "+" : like Current prefix "-" : like Current infix "-" (other : like Current) : like Current infix "/" (other : like Current) : like Current infix "^" (exp : INTEGER) : like Current is_invertible : BOOLEAN one : like Current valid_divisor (other : like Current) : BOOLEAN zero : like Current inherited features -- From ADDABLE: infix "+", prefix "+", infix "-", prefix "-", zero feature specification infix "*" (other : like Current) : like Current -- Product of `Current' by `other' require other_not_void : other /= void; deferred ensure not_void : Result /= void; infix "/" (other : like Current) : like Current -- Division of `Current' by `other' require other_not_void : other /= void; divisible : valid_divisor (other); deferred ensure not_void : Result /= void; infix "^" (exp : INTEGER) : like Current -- Raise Current to `exp'-th power -- -- NOTE: The signature of `infix "^"' is different from the one -- listed in ETL. Our infix "^" supports only INTEGER exponents. -- Raising to integral powers is a reasonable feature for all numeric -- descendents (e.g., SQUARE_MATRIX), while raising to a non-integral -- exponent might not be. `power' in REAL_REF and DOUBLE_REF -- implements the semantics of the `infix "^"' operator listed in ETL -- (that is, it supports positive non-integral exponents). require acceptable : (exp >= 0) or else is_invertable; ensure not_void : Result /= void; consistent : (((exp > 0) and then Result.is_equal ((Current ^ (exp - 1)) * Current)) or else ((exp = 0) and then Result.is_equal (one))) or else ((exp < 0) and then Result.is_equal (one / (Current ^ (- exp)))); is_invertible : BOOLEAN -- Does multiplicative inverse of `Current' exist? ensure divides_one : Result = one.valid_divisor (Current); valid_divisor (other : like Current) : BOOLEAN -- Can `Current' be divided by other? require non_void : other /= void; deferred one : like Current -- The neutral element of multiplication deferred ensure not_void : Result /= void; end interface -- class NUMERIC -- Numeric elements that may be compared for a total order relation. -- -- Inheritance: -- COMPARABLE; -- NUMERIC deferred class interface COMPARABLE_NUMERIC ancestors COMPARABLE_NUMERIC COMPARABLE PART_COMPARABLE NUMERIC ADDABLE feature summary infix "*" (other : like Current) : like Current prefix "+" : like Current infix "+" (other : like Current) : like Current prefix "-" : like Current infix "-" (other : like Current) : like Current infix "/" (other : like Current) : like Current infix "<" (other : like Current) : BOOLEAN infix "<=" (other : like Current) : BOOLEAN infix ">" (other : like Current) : BOOLEAN infix ">=" (other : like Current) : BOOLEAN infix "^" (exp : INTEGER) : like Current is_invertible : BOOLEAN max (other : like Current) : like Current min (other : like Current) : like Current one : like Current relative_to (other : like Current) : INTEGER valid_divisor (other : like Current) : BOOLEAN zero : like Current inherited features -- From COMPARABLE: infix "<", infix "<=", max, min, relative_to -- From PART_COMPARABLE: infix ">", infix ">=" -- From NUMERIC: infix "*", infix "/", infix "^", is_invertible, one, valid_divisor -- From ADDABLE: infix "+", prefix "+", infix "-", prefix "-", zero end interface -- class COMPARABLE_NUMERIC -- Hashable elements -- -- Inheritance: -- -- none deferred class interface HASHABLE ancestors HASHABLE feature summary hash_code : INTEGER feature specification hash_code : INTEGER -- Hash_code value deferred ensure non_negative : Result >= 0; end interface -- class HASHABLE -- Character strings. -- -- Inheritance: -- HASHABLE -- redefine -- is_equal, copy, to_string -- end; -- -- COMPARABLE -- redefine -- is_equal, copy, to_string, relative_to, infix ">" -- end; class interface STRING ancestors STRING HASHABLE COMPARABLE PART_COMPARABLE feature summary infix "+" (other : like Current) : like Current infix "<" (other : like Current) : BOOLEAN infix "<=" (other : like Current) : BOOLEAN infix ">" (other : like Current) : BOOLEAN infix ">=" (other : like Current) : BOOLEAN infix "@" (i : INTEGER) : CHARACTER adapt (other : STRING) append (s : like Current) copy (other : like Current) count : INTEGER empty : BOOLEAN extend (c : CHARACTER) force (c : CHARACTER; i : INTEGER) force_range (s : like Current; i : INTEGER) hash_code : INTEGER insert (c : CHARACTER; i : INTEGER) insert_range (s : like Current; i : INTEGER) is_equal (other : like Current) : BOOLEAN item (i : INTEGER) : CHARACTER item_range (lower_index, upper_index : INTEGER) : like Current make (n : INTEGER) make_from_pointer (c_string : POINTER) max (other : like Current) : like Current min (other : like Current) : like Current move (lower_source, upper_source, destination : INTEGER) precede (c : CHARACTER) prepend (s : like Current) put (c : CHARACTER; i : INTEGER) put_range (s : like Current; i : INTEGER) relative_to (other : like Current) : INTEGER remove (i : INTEGER) remove_range (lower_index, upper_index : INTEGER) to_external : POINTER to_lower to_string : STRING to_upper valid_index (i : INTEGER) : BOOLEAN creation adapt, make, make_from_pointer inherited features -- From COMPARABLE: infix "<=", max, min -- From PART_COMPARABLE: infix ">=" feature specification -- Creation make (n : INTEGER) -- Allocate an empty string with space for at least `n' -- characters. Note: `n' is a hint of the expected size of -- the new string. An implementation might use it to -- preallocate an `area' of the given size. Another -- implementation might ignore the hint. require non_negative_size : n >= 0; ensure count = 0; make_from_pointer (c_string : POINTER) -- Make an Eiffel string which is a copy of the C string -- `c_string' require c_string_not_null : c_string /= null_pointer; adapt (other : STRING) -- Initialize `Current's character array from `other'. -- Intended to be used as a creation procedure in -- descendents of STRING. require other_not_void : other /= void; ensure same_text : -- the text of Current is the same as the text -- of `other'. feature specification -- From GENERAL: copy (other : like Current) -- Copy all characters from `other' to `Current'. require other_not_void : other /= void; ensure -- for all `i: 1..count, Result.item (i) = item (i)' is_equal : is_equal (other); is_equal (other : like Current) : BOOLEAN -- Is `Current' made of the same character sequence as -- `other'? require other_not_void : other /= void; ensure counts : Result implies (count = other.count); to_string : STRING -- Printable representation of current string ensure not_void : Result /= void; feature specification -- From COMPARABLE: infix "<" (other : like Current) : BOOLEAN -- Is `Current' lexicographically less than than `other'? -- Effects deferred feature from COMPARABLE. require other_not_void : other /= void; ensure other_not_less_or_equal : Result = (not (other <= Current)); consistent : Result implies (not (other <= Current)); not_reflexive : (Current = other) implies (not Result); infix ">" (other : like Current) : BOOLEAN -- Is `Current' lexicographically less than than `other'? require other_not_void : other /= void; ensure other_is_less : Result = (other < Current); relative_to (other : like Current) : INTEGER -- The relative position of `Current' to `other': -- `< 0' if `Current < other'; -- `0' if `Current = other'; -- `> 0' if `Current > other'. require other_not_void : other /= void; ensure negative_condition : (Result < 0) = (Current < other); zero_condition : (Result = 0) = (not ((Current < other) or (Current > other))); positive_condition : (Result > 0) = (Current > other); feature specification -- Features which may potentially inherit from an ancestor common to -- STRING, ARRAY and BIT_REF. infix "@", item (i : INTEGER) : CHARACTER -- Character at position `i' require valid_index : valid_index (i); put (c : CHARACTER; i : INTEGER) -- Replace the character at position `i' by `c'. require valid_index : valid_index (i); ensure value_in_place : item (i) = c; valid_index (i : INTEGER) : BOOLEAN -- Is `i' a valid index for the current string? count : INTEGER -- Actual number of characters making up the string. ensure Result >= 0; empty : BOOLEAN -- Is Current an empty string? ensure count : Result = (count = 0); feature specification -- Features which are similar between ARRAY and STRING item_range (lower_index, upper_index : INTEGER) : like Current -- String containing characters in the range [`lower_index' -- .. `upper_index']; empty if upper_index = lower_index - 1. require valid_lower : valid_index (lower_index); valid_upper : (upper_index >= (lower_index - 1)) and (upper_index <= upper); ensure not_void : Result /= void; count : Result.count = ((upper_index - lower_index) + 1); same_items : -- for all `i: 1..upper_index-lower_index + 1', -- `Result.item (i) = item (lower_index+i-1)' put_range (s : like Current; i : INTEGER) -- Replace the characters starting at position `i' with the -- characters in `s'. This routine will tolerate -- destinations that extend off the bounds of the string. -- If the destination range extends off the end of the -- string, the string is not resized. require valid_string : s /= void; valid_index : valid_index (i); ensure same_size : (old count) = count; insert (c : CHARACTER; i : INTEGER) -- Insert `c' at position `i'. require valid_index : valid_index (i); ensure inserted : item (i) = c; lengthened : count = ((old count) + 1); -- Items previously at positions `i .. count' -- have moved one position towards higher indices. insert_range (s : like Current; i : INTEGER) -- Insert a copy of `s' starting at position `i'. require valid_index : valid_index (i); ensure lengthened : count = ((old count) + 1); -- Items previously at positions `i .. count' -- have moved `s.count' positions towards higher indices. -- Items from `s' have been copied into positions `i .. i + -- s.count - 1'. remove (i : INTEGER) -- Remove character at position `i'. require valid_index : valid_index (i); ensure removed : -- The character at position `i' has been removed. shortened : count = ((old count) - 1); remove_range (lower_index, upper_index : INTEGER) -- Remove characters in positions `lower_index .. -- upper_index'. require valid_lower : valid_index (lower_index); valid_upper : valid_index (upper_index); valid_range : lower_index <= upper_index; ensure removed : -- The characters at positions `lower_index .. -- upper_index' have been removed. shortened : count = ((((old count) - upper_index) + lower_index) - 1); force (c : CHARACTER; i : INTEGER) -- Assign `c' to `i'-th character. Always applicable: resize -- the string if `i' falls out of currently defined bounds. -- During resizing, preserve existing characters, and fill -- new positions with spaces. ensure item_in_place : item (i) = c; valid_index : valid_index (i); force_range (s : like Current; i : INTEGER) -- Copy the characters in `s' to the positions starting at -- `i'. Always applicable: resize the array if `i + s.count -- - 1' falls out of currently defined bounds. During -- resizing, preserve existing characters, and fill new -- positions with spaces. require valid_string : s /= void; ensure valid_index : valid_index ((i + s.count) - 1); precede (c : CHARACTER) -- Add `c' at front. ensure count = ((old count) + 1); value_in_place : item (1) = c; prepend (s : like Current) -- Prepend a copy of `s' at front of `Current'. require argument_not_void : s /= void; ensure count = ((old count) + s.count); extend (c : CHARACTER) -- Add `c' at end. ensure count = ((old count) + 1); value_in_place : item (count) = c; append (s : like Current) -- Append a copy of `s' at end of `Current'. require argument_not_void : s /= void; ensure count = ((old count) + s.count); move (lower_source, upper_source, destination : INTEGER) -- Move the characters in the range `lower_source .. -- upper_source' to the positions starting at `destination'. -- Items in the destination area are written over. The two -- ranges may overlap. This routine will tolerate -- destinations that extend off the bounds of the string. -- Elements in the source range are not changed (unless they -- are also in the destination range). If the destination -- range extends off the end of the string, those elements -- are not copied: the string is not resized. require valid_from : valid_index (lower_source); valid_to : valid_index (upper_source); ensure same_size : (old count) = count; feature specification infix "+" (other : like Current) : like Current -- Return a new string which is the concatenation of -- `Current' and `other'. require argument_not_void : other /= void; ensure not_void : Result /= void; to_lower -- Convert string to lower case. to_upper -- Convert string to upper case. hash_code : INTEGER -- Hash code value of `Current' ensure non_negative : Result >= 0; to_external : POINTER -- Corresponding null-terminated C string. -- Note: named `to_c' in ETL/2. invariant positive_count : 0 <= count; end interface -- class STRING -- One-dimensional arrays with element type `Element_T'. -- -- Inheritance: -- ANY -- redefine -- is_equal, copy -- end class interface ARRAY [Element_T] ancestors ARRAY [Element_T] feature summary infix "@" (i : INTEGER) : Element_T adapt (other : ARRAY [Element_T]) append (r : like Current) copy (other : like Current) count : INTEGER empty : BOOLEAN extend (v : like item) force (v : like item; i : INTEGER) force_range (r : like Current; i : INTEGER) insert (v : like item; i : INTEGER) insert_range (r : like Current; i : INTEGER) is_equal (other : like Current) : BOOLEAN item (i : INTEGER) : Element_T item_range (lower_index, upper_index : INTEGER) : like Current lower : INTEGER make (minindex, maxindex : INTEGER) move (lower_source, upper_source, destination : INTEGER) precede (v : like item) prepend (v : like Current) put (v : like item; i : INTEGER) put_range (r : like Current; i : INTEGER) reindex (new_lower : INTEGER) remove (i : INTEGER) remove_range (lower_index, upper_index : INTEGER) resize (new_lower, new_upper : INTEGER) to_external : POINTER upper : INTEGER valid_index (i : INTEGER) : BOOLEAN creation make, adapt feature specification -- Creation make (minindex, maxindex : INTEGER) -- If `minindex' <= `maxindex', allocate array with bounds -- `minindex' and `maxindex'; otherwise create empty array. require meaningful_count : maxindex >= (minindex - 1); ensure lower_is_min : lower = minindex; upper_is_max : upper = maxindex; adapt (other : ARRAY [Element_T]) -- Initialize `Current's array from `other'. Intended to be -- used as a creation procedure in descendents of ARRAY, -- so that the descendant can initialize itself with a -- manifest array (which would not conform to like Current -- in a descendant). require other_not_void : other /= void; ensure same_lower : lower = other.lower; same_upper : upper = other.upper; same_items : -- the items of Current are the same as the -- items of `other'. feature specification -- From GENERAL copy (other : like Current) -- Make `Current' an element-by-element copy of `other'. require other_not_void : other /= void; ensure is_equal : is_equal (other); is_equal (other : like Current) : BOOLEAN -- Is `Current' element-by-element equal to `other'? -- Redefined from `GENERAL'. require other_not_void : other /= void; ensure same_bounds : Result implies ((lower = other.lower) and (upper = other.upper)); -- `Result implies For all i: lower .. upper, item(i) = other.item(i)' feature specification -- Features which may potentially inherit from an ancestor common to -- STRING, ARRAY and BIT_REF. item, infix "@" (i : INTEGER) : Element_T -- Entry of index `i'. -- Applicable only if `i' is between `lower' and `upper'. require valid_index : valid_index (i); valid_index (i : INTEGER) : BOOLEAN -- Is `i' between currently defined bounds? ensure (Result = (lower <= i)) and (i <= upper); put (v : like item; i : INTEGER) -- Replace `i'-th entry by `v'. -- Applicable only if `i' is between `lower' and `upper'. require valid_index : valid_index (i); ensure value_in_place : item (i) = v; count : INTEGER -- Number of available indices empty : BOOLEAN -- Is current an empty array? ensure count : Result = (count = 0); feature specification -- Features which are similar between ARRAY and STRING item_range (lower_index, upper_index : INTEGER) : like Current -- Array containing items in the range [`lower_index' .. -- `upper_index']; empty if upper_index = lower_index - 1. require valid_lower : valid_index (lower_index); valid_upper : (upper_index >= (lower_index - 1)) and (upper_index <= upper); ensure not_void : Result /= void; same_lower : Result.lower = lower_index; same_upper : Result.upper = upper_index; same_items : -- for all `i: 1..upper_index-lower_index', -- `Result.item (i) = item (lower_index+i-1)' put_range (r : like Current; i : INTEGER) -- Replace the items starting at `i' with the items in `r'. -- This routine will tolerate destinations that extend off -- the bounds of the array. If the destination range extends -- off the end of the array, the array is not resized. require valid_range : r /= void; valid_index : valid_index (i); ensure same_size : (old count) = count; insert (v : like item; i : INTEGER) -- Insert `v' at position `i'. require valid_index : valid_index (i); ensure inserted : item (i) = v; lengthened : count = ((old count) + 1); -- Items previously at positions `index .. count' -- have moved one position towards higher indices. insert_range (r : like Current; i : INTEGER) -- Insert a copy of `r' starting at position `i'. require valid_index : valid_index (i); ensure lengthened : count = ((old count) + r.count); -- Items previously at positions `index .. count' have -- moved `r.count' positions towards higher indices. Items -- from `r' now occupy positions `i .. i + r.count - 1'. remove (i : INTEGER) -- Remove item at position `i'. require valid_index : valid_index (i); ensure removed : -- The item at position `index' has been removed. shortened : count = ((old count) - 1); remove_range (lower_index, upper_index : INTEGER) -- Remove items within the range `lower_index .. -- upper_index'. require valid_lower : valid_index (lower_index); valid_upper : valid_index (upper_index); valid_range : lower_index <= upper_index; ensure removed : -- The items at positions `lower_index .. -- upper_index' have been removed. shortened : count = ((((old count) - upper_index) + lower_index) - 1); force (v : like item; i : INTEGER) -- Assign item `v' to `i'-th item. Always applicable: resize -- the array if `i' falls out of currently defined bounds. -- During resizing, preserve existing elements. ensure item_in_place : item (i) = v; valid_index : valid_index (i); force_range (r : like Current; i : INTEGER) -- Assign the items in `r' to positions starting at `i'. -- Always applicable: resize the array if `i' or `i + -- r.count - 1' falls out of currently defined bounds. -- During resizing, preserve existing elements. require valid_range : r /= void; ensure valid_index : valid_index (i) and valid_index ((i + r.count) - 1); precede (v : like item) -- Add `v' at front. ensure lower_decreased : lower = ((old lower) - 1); upper_unchanged : upper = (old upper); value_in_place : item (lower) = v; prepend (v : like Current) -- Prepend a copy of `r' at front of `Current'. require argument_not_void : r /= void; ensure lower_decreased : lower = ((old lower) - r.count); upper_unchanged : upper = (old upper); extend (v : like item) -- Add `v' at end. ensure lower_unchanged : lower = (old lower); upper_increased : upper = ((old upper) + 1); value_in_place : item (upper) = v; append (r : like Current) -- Append a copy of `r' at end of `Current'. require argument_not_void : r /= void; ensure lower_unchanged : lower = (old lower); upper_increased : upper = ((old upper) + r.count); move (lower_source, upper_source, destination : INTEGER) -- Move the items in the range `lower_source .. -- upper_source' to the sequence starting at `destination'. -- Items in the destination area are written over. The two -- ranges may overlap. This routine will tolerate desti- -- nations that extend off the bounds of the array. Elements -- in the source range are not changed (unless they are also -- in the destination range). If the destination range -- extends off the end of the array, those elements are not -- copied: the array is not resized. require valid_from : valid_index (lower_source); valid_to : valid_index (upper_source); ensure same_size : (old count) = count; feature specification resize (new_lower, new_upper : INTEGER) -- Rearrange array so that it can accommodate indices down -- to `new_lower' and up to `new_upper'. Elements will not -- be lost in the intersection of `lower .. upper' and -- `new_lower .. new_upper'. New positions will be -- initialized with the appropriate default values. require meaningful_count : new_upper >= (new_lower - 1); ensure new_lower : lower = new_lower; new_upper : new_upper = upper; same_position : -- An element that was previously at -- position `i' remains at position `i' if -- `i' is within the new bounds. reindex (new_lower : INTEGER) -- Change index interval so that it starts at `new_lower'. -- No elements will be lost. ensure new_lower : lower = new_lower; new_upper : upper = ((new_lower + count) - 1); to_external : POINTER -- Address of the actual sequence of values for passing to -- foreign (non-Eiffel) routines. Note: Return type is -- `POINTER' instead of `NONE' as specified in ETL. upper : INTEGER -- Maximum current legal index. lower : INTEGER -- Minimum current legal index. invariant non_negative_size : count >= 0; end interface -- class ARRAY ================================================== Date: Sat, 30 Jul 94 18:16:08 EDT >From: gustave Subject: Gustave Kernel (9/9): Shorts (2/2) -- Reference version of BIT `n' types. -- -- Inheritance: -- ANY -- redefine -- is_equal, copy -- end class interface BIT_REF ancestors BIT_REF feature summary infix "#" (s : INTEGER) : like Current infix "@" (i : INTEGER) : BOOLEAN infix "^" (s : INTEGER) : like Current infix "and" (other : like Current) : like Current copy (other : like Current) count : INTEGER infix "implies" (other : like Current) : like Current is_equal (other : like Current) : BOOLEAN item (i : INTEGER) : BOOLEAN make (n : INTEGER) prefix "not" : like Current infix "or" (other : like Current) : like Current put (value : BOOLEAN; i : INTEGER) valid_index (i : INTEGER) : BOOLEAN infix "xor" (other : like Current) : like Current creation make feature specification make (n : INTEGER) -- Create a new BIT_REF that contains `n' 0 bits. require positive_count : n >= 0; ensure count : count = n; feature specification -- Features which may potentially inherit from an ancestor common to -- STRING, ARRAY and BIT_REF. put (value : BOOLEAN; i : INTEGER) -- Set the `i'th bit to 1 if `value' is True, 0 if False. require valid_index : valid_index (i); ensure value_in_place : item (i) = value; item, infix "@" (i : INTEGER) : BOOLEAN -- `i'th bit. require valid_index : valid_index (i); valid_index (i : INTEGER) : BOOLEAN -- Is `i' a valid index for `Current'? feature specification infix "^" (s : INTEGER) : like Current -- Result of shifting bit sequence by `s' positions -- (Positive `s' shifts right, negative `s' shifts left; -- bits failing off the sequence's bounds are lost.) ensure not_void : Result /= void; infix "#" (s : INTEGER) : like Current -- Result of rotating bit sequence by `s' positions -- (Positive `s' rotates right, negative `s' rotates left.) ensure not_void : Result /= void; infix "and" (other : like Current) : like Current -- Conjunction with `other' require other_exists : other /= void; conformance : other.count <= count; ensure not_void : Result /= void; infix "implies" (other : like Current) : like Current -- Implication of `other' require other_exists : other /= void; conformance : other.count <= count; ensure not_void : Result /= void; infix "or" (other : like Current) : like Current -- Disjunction with `other' require other_exists : other /= void; conformance : other.count <= count; ensure not_void : Result /= void; infix "xor" (other : like Current) : like Current -- Exclusive or with `other' require other_exists : other /= void; conformance : other.count <= count; ensure not_void : Result /= void; prefix "not" : like Current -- Negation ensure not_void : Result /= void; feature specification -- Bit size count : INTEGER -- Size of the current bit object (the `n' in `BIT n'). feature specification -- Redefinitions of GENERAL's standard routines is_equal (other : like Current) : BOOLEAN -- Is `other' bit-by-bit identical to `Current'? require other_not_void : other /= void; copy (other : like Current) -- Copy every field of `other' into corresponding field of `Current'. require other_not_void : other /= void; ensure is_equal : is_equal (other); end interface -- class BIT_REF -- Pseudo-class for basic type BOOLEAN. -- -- Inheritance: -- BOOLEAN_REF -- export {NONE} make -- end; expanded class interface BOOLEAN ancestors BOOLEAN BOOLEAN_REF feature summary infix "and" (other : like Current) : like Current infix "and then" (other : like Current) : like Current infix "implies" (other : like Current) : like Current item : BOOLEAN prefix "not" : like Current infix "or" (other : like Current) : like Current infix "or else" (other : like Current) : like Current to_string : STRING infix "xor" (other : like Current) : like Current inherited features -- From BOOLEAN_REF: infix "and", infix "and then", infix "implies", item, prefix "not", infix "or", infix "or else", to_string, infix "xor" end interface -- class BOOLEAN -- Reference version of the basic type BOOLEAN. -- -- Inheritance: -- ANY -- redefine -- to_string -- end; class interface BOOLEAN_REF ancestors BOOLEAN_REF feature summary infix "and" (other : like Current) : like Current infix "and then" (other : like Current) : like Current infix "implies" (other : like Current) : like Current item : BOOLEAN make (b : BOOLEAN) prefix "not" : like Current infix "or" (other : like Current) : like Current infix "or else" (other : like Current) : like Current to_string : STRING infix "xor" (other : like Current) : like Current creation make feature specification make (b : BOOLEAN) -- Make a BOOLEAN_REF from BOOLEAN `b'. ensure item_set : item = b; item : BOOLEAN -- The value of this reference to_string : STRING -- New string containing a printable representation of `item' ensure not_void : Result /= void; infix "and" (other : like Current) : like Current -- Boolean conjunction of `Current' and `other' require other_not_void : other /= void; ensure not_void : Result /= void; infix "and then" (other : like Current) : like Current -- Boolean non-strict conjunction of `Current' and `other' require other_not_void : other /= void; ensure not_void : Result /= void; infix "implies" (other : like Current) : like Current -- Boolean semi-strict implication of `Current' and `other' require other_not_void : other /= void; ensure not_void : Result /= void; prefix "not" : like Current -- Negation of `Current' ensure not_void : Result /= void; infix "or" (other : like Current) : like Current -- Boolean disjunction of `Current' and `other' require other_not_void : other /= void; ensure not_void : Result /= void; infix "or else" (other : like Current) : like Current -- Boolean non-strict disjunction of `Current' and `other' require other_not_void : other /= void; ensure not_void : Result /= void; infix "xor" (other : like Current) : like Current -- Boolean exclusive or of `Current' and `other' require other_not_void : other /= void; ensure not_void : Result /= void; end interface -- class BOOLEAN_REF -- Pseudo-class for basic type CHARACTER. -- -- Inheritance: -- CHARACTER_REF -- export {NONE} make -- end expanded class interface CHARACTER ancestors CHARACTER CHARACTER_REF COMPARABLE PART_COMPARABLE HASHABLE feature summary infix "<" (other : like Current) : BOOLEAN infix "<=" (other : like Current) : BOOLEAN infix ">" (other : like Current) : BOOLEAN infix ">=" (other : like Current) : BOOLEAN hash_code : INTEGER is_alpha : BOOLEAN is_alphanumeric : BOOLEAN is_control : BOOLEAN is_digit : BOOLEAN is_lower : BOOLEAN is_printable : BOOLEAN is_upper : BOOLEAN is_whitespace : BOOLEAN item : CHARACTER max (other : like Current) : like Current min (other : like Current) : like Current relative_to (other : like Current) : INTEGER to_integer : INTEGER to_lower : like Current to_string : STRING to_upper : like Current inherited features -- From CHARACTER_REF: infix "<", hash_code, is_alpha, is_alphanumeric, is_control, is_digit, is_lower, is_printable, is_upper, is_whitespace, item, to_integer, to_lower, to_string, to_upper -- From COMPARABLE: infix "<=", max, min, relative_to -- From PART_COMPARABLE: infix ">", infix ">=" end interface -- class CHARACTER -- Reference version of the basic type CHARACTER. -- -- Inheritance: -- COMPARABLE -- redefine -- to_string -- end; -- -- HASHABLE -- redefine -- hash_code -- end; class interface CHARACTER_REF ancestors CHARACTER_REF COMPARABLE PART_COMPARABLE HASHABLE feature summary infix "<" (other : like Current) : BOOLEAN infix "<=" (other : like Current) : BOOLEAN infix ">" (other : like Current) : BOOLEAN infix ">=" (other : like Current) : BOOLEAN hash_code : INTEGER is_alpha : BOOLEAN is_alphanumeric : BOOLEAN is_control : BOOLEAN is_digit : BOOLEAN is_lower : BOOLEAN is_printable : BOOLEAN is_upper : BOOLEAN is_whitespace : BOOLEAN item : CHARACTER make (ch : CHARACTER) max (other : like Current) : like Current min (other : like Current) : like Current relative_to (other : like Current) : INTEGER to_integer : INTEGER to_lower : like Current to_string : STRING to_upper : like Current creation make inherited features -- From COMPARABLE: infix "<=", max, min, relative_to -- From PART_COMPARABLE: infix ">", infix ">=" feature specification item : CHARACTER -- The value of this reference make (ch : CHARACTER) -- Make a CHARACTER_REF from CHARACTER `ch'. ensure item_set : item = ch; to_string : STRING -- New string containing a printable representation of `item' ensure not_void : Result /= void; feature specification -- Conversion features to_lower : like Current -- If `Current' is a uppercase character, return the lowercase -- equivalent, else return `Current'. ensure not_void : Result /= void; to_upper : like Current -- If `Current' is a lowercase character, return the uppercase -- equivalent, else return `Current'. ensure not_void : Result /= void; to_integer : INTEGER -- Return the numeric code of `Current'. ensure non_negative : Result >= 0; feature specification -- Character classification is_alphanumeric : BOOLEAN -- Is the character a letter or number? is_digit : BOOLEAN -- Is the character a number? is_alpha : BOOLEAN -- Is the character a letter? is_lower : BOOLEAN -- Is the character a lowercase letter? is_upper : BOOLEAN -- Is the character an uppercase letter? is_whitespace : BOOLEAN -- Is the character a space, tab or newline? is_printable : BOOLEAN -- Is the character a printing character (not a control character)? is_control : BOOLEAN -- Is the character a non-printing control character? feature specification -- From COMPARABLE infix "<" (other : like Current) : BOOLEAN -- Is `Current' less than `other'? require other_not_void : other /= void; ensure other_not_less_or_equal : Result = (not (other <= Current)); consistent : Result implies (not (other <= Current)); not_reflexive : (Current = other) implies (not Result); feature specification -- From HASHABLE hash_code : INTEGER -- Hash_code value ensure non_negative : Result >= 0; end interface -- class CHARACTER_REF -- Reference version of the basic type DOUBLE. -- -- Inheritance: -- COMPARABLE_NUMERIC -- redefine -- to_string, infix "^", infix "-", zero -- end; class interface DOUBLE_REF ancestors DOUBLE_REF COMPARABLE_NUMERIC COMPARABLE PART_COMPARABLE NUMERIC ADDABLE feature summary infix "*" (other : like Current) : like Current prefix "+" : like Current infix "+" (other : like Current) : like Current prefix "-" : like Current infix "-" (other : like Current) : like Current infix "/" (other : like Current) : like Current infix "<" (other : like Current) : BOOLEAN infix "<=" (other : like Current) : BOOLEAN infix ">" (other : like Current) : BOOLEAN infix ">=" (other : like Current) : BOOLEAN infix "^" (other : INTEGER) : like Current abs : like Current ceiling : like Current floor : like Current is_invertible : BOOLEAN item : DOUBLE make (d : DOUBLE) max (other : like Current) : like Current min (other : like Current) : like Current one : like Current power (other : like Current) : like Current relative_to (other : like Current) : INTEGER round : like Current round_to_zero : like Current sign : INTEGER to_integer : INTEGER to_real : REAL to_string : STRING valid_divisor (other : like Current) : BOOLEAN zero : like Current creation make inherited features -- From COMPARABLE: infix "<=", max, min, relative_to -- From PART_COMPARABLE: infix ">", infix ">=" -- From NUMERIC: is_invertible -- From ADDABLE: prefix "+" feature specification item : DOUBLE -- The value of this reference make (d : DOUBLE) -- Make a DOUBLE_REF from DOUBLE `d'. ensure item_set : item = d; to_string : STRING -- New string containing a printable representation of `item' ensure not_void : Result /= void; feature specification -- Power infix "^" (other : INTEGER) : like Current -- Raise `Current' to the power `other'? See also `power' below. require acceptable : (other >= 0) or else is_invertable; ensure not_void : Result /= void; consistent : (((other > 0) and then Result.is_equal ((Current ^ (other - 1)) * Current)) or else ((other = 0) and then Result.is_equal (one))) or else ((other < 0) and then Result.is_equal (one / (Current ^ (- other)))); power (other : like Current) : like Current -- Raise `Current' to the power `other'? See also `infix "^"' above. require positive : item > 0.0; ensure not_void : Result /= void; feature specification -- From COMPARABLE: infix "<" (other : like Current) : BOOLEAN -- Is `Current' less than `other'? require other_not_void : other /= void; ensure other_not_less_or_equal : Result = (not (other <= Current)); consistent : Result implies (not (other <= Current)); not_reflexive : (Current = other) implies (not Result); feature specification -- From NUMERIC: infix "+" (other : like Current) : like Current -- Sum of `Current' and `other' require other_not_void : other /= void; ensure not_void : Result /= void; commutative : Result.is_equal (other + Current); infix "-" (other : like Current) : like Current -- Difference between `Current' and `other' require other_not_void : other /= void; ensure not_void : Result /= void; consistent : Result.is_equal (Current + (- other)); infix "*" (other : like Current) : like Current -- Product of `Current' by `other' require other_not_void : other /= void; ensure not_void : Result /= void; infix "/" (other : like Current) : like Current -- Division of `Current' by `other' require other_not_void : other /= void; divisible : valid_divisor (other); ensure not_void : Result /= void; prefix "-" : like Current -- Unary subtraction applied to `Current' ensure not_void : Result /= void; idempotent : (- Result).is_equal (Current); feature specification valid_divisor (other : like Current) : BOOLEAN -- Can `Current' be divided by `other'? require non_void : other /= void; one : like Current -- The neutral element of multiplication ensure not_void : Result /= void; zero : like Current -- The neutral element of addition ensure not_void : Result /= void; consistent : Result.is_equal (Current - Current); feature specification -- Additional comparison features sign : INTEGER -- Sign of `Current': -- -1 if `Current < zero' -- 0 if `Current = zero' -- 1 if `Current > zero' ensure negative_condition : (Result = (- 1)) = (Current < zero); zero_condition : (Result = 0) = (not ((Current < zero) or (Current > zero))); positive_condition : (Result = 1) = (Current > zero); abs : like Current -- The absolute value of `Current' ensure not_void : Result /= void; same_as_negative : (Current < zero) = (relative_to (- Result) = 0); same_if_positive : (Current >= zero) = (relative_to (Result) = 0); feature specification -- Conversion features to_real : REAL -- Convert `Current' to its equivalent as a REAL. If `Current's value -- cannot be represented as a REAL, the result is undefined. to_integer : INTEGER -- Convert `Current' to an integer, discarding the any non-integral -- portion of `Current's value (ie., truncate). To control the -- truncation behavior, use in conjunction with `floor', `ceiling', -- `round' or `round_to_zero' (e.g., `value.round.to_integer'). floor : like Current -- The greatest integral value less than or equal to `Current' ensure not_void : Result /= void; ceiling : like Current -- The least integral value greater than or equal to `Current' ensure not_void : Result /= void; round : like Current -- The rounded integral value of `Current'. If `Current = 0.5', -- returns `ceiling'. ensure not_void : Result /= void; round_to_zero : like Current -- The rounded integral value of `Current'. If `Current = 0.5', -- returns `floor'. ensure not_void : Result /= void; end interface -- class DOUBLE_REF -- Pseudo-class for basic type DOUBLE. -- -- Inheritance: -- DOUBLE_REF -- export {NONE} make -- end; expanded class interface DOUBLE ancestors DOUBLE DOUBLE_REF COMPARABLE_NUMERIC COMPARABLE PART_COMPARABLE NUMERIC ADDABLE feature summary infix "*" (other : like Current) : like Current prefix "+" : like Current infix "+" (other : like Current) : like Current prefix "-" : like Current infix "-" (other : like Current) : like Current infix "/" (other : like Current) : like Current infix "<" (other : like Current) : BOOLEAN infix "<=" (other : like Current) : BOOLEAN infix ">" (other : like Current) : BOOLEAN infix ">=" (other : like Current) : BOOLEAN infix "^" (other : INTEGER) : like Current abs : like Current ceiling : like Current floor : like Current is_invertible : BOOLEAN item : DOUBLE max (other : like Current) : like Current min (other : like Current) : like Current one : like Current power (other : like Current) : like Current relative_to (other : like Current) : INTEGER round : like Current round_to_zero : like Current sign : INTEGER to_integer : INTEGER to_real : REAL to_string : STRING valid_divisor (other : like Current) : BOOLEAN zero : like Current inherited features -- From DOUBLE_REF: infix "*", infix "+", prefix "-", infix "-", infix "/", infix "<", infix "^", abs, ceiling, floor, item, one, power, round, round_to_zero, sign, to_integer, to_real, to_string, valid_divisor, zero -- From COMPARABLE: infix "<=", max, min, relative_to -- From PART_COMPARABLE: infix ">", infix ">=" -- From NUMERIC: is_invertible -- From ADDABLE: prefix "+" end interface -- class DOUBLE -- Reference version of the basic type INTEGER. -- -- Inheritance: -- COMPARABLE_NUMERIC -- rename -- infix"/" as infix"//" -- redefine -- to_string, infix "^", infix"//", infix "-", zero -- end; -- -- HASHABLE -- redefine -- to_string -- end; class interface INTEGER_REF ancestors INTEGER_REF COMPARABLE_NUMERIC COMPARABLE PART_COMPARABLE NUMERIC ADDABLE HASHABLE feature summary infix "*" (other : like Current) : like Current prefix "+" : like Current infix "+" (other : like Current) : like Current infix "-" (other : like Current) : like Current prefix "-" : like Current infix "/" (other : like Current) : REAL infix "//" (other : like Current) : like Current infix "<" (other : like Current) : BOOLEAN infix "<=" (other : like Current) : BOOLEAN infix ">" (other : like Current) : BOOLEAN infix ">=" (other : like Current) : BOOLEAN infix "\\" (other : like Current) : like Current infix "^" (exp : INTEGER) : like Current hash_code : INTEGER is_invertible : BOOLEAN item : INTEGER make (i : INTEGER) max (other : like Current) : like Current min (other : like Current) : like Current one : like Current relative_to (other : like Current) : INTEGER to_character : CHARACTER to_double : DOUBLE to_real : REAL to_string : STRING valid_divisor (other : like Current) : BOOLEAN zero : like Current creation make inherited features -- From COMPARABLE: infix "<=", max, min, relative_to -- From PART_COMPARABLE: infix ">", infix ">=" -- From NUMERIC: is_invertible -- From ADDABLE: prefix "+" feature specification item : INTEGER -- The value of this reference to_string : STRING -- New string containing a printable representation of `item' ensure not_void : Result /= void; make (i : INTEGER) -- Make an INTEGER_REF from INTEGER `i'. ensure item_set : item = i; infix "//" (other : like Current) : like Current -- Integer division of `Current' by `other'? require other_not_void : other /= void; divisible : valid_divisor (other); ensure not_void : Result /= void; infix "\\" (other : like Current) : like Current -- Remainder of integer division of `Current' by `other'? require non_void : other /= void; non_zero_divisor : other.item /= 0; feature specification -- From HASHABLE: hash_code : INTEGER -- Hash code value ensure non_negative : Result >= 0; feature specification -- From COMPARABLE: infix "<" (other : like Current) : BOOLEAN -- Is `Current' less than `other'? require other_not_void : other /= void; ensure other_not_less_or_equal : Result = (not (other <= Current)); consistent : Result implies (not (other <= Current)); not_reflexive : (Current = other) implies (not Result); feature specification -- From NUMERIC: infix "+" (other : like Current) : like Current -- Sum of `Current' and `other' require other_not_void : other /= void; ensure not_void : Result /= void; commutative : Result.is_equal (other + Current); infix "-" (other : like Current) : like Current -- Difference between `Current' and `other' require other_not_void : other /= void; ensure not_void : Result /= void; consistent : Result.is_equal (Current + (- other)); infix "*" (other : like Current) : like Current -- Product of `Current' by `other' require other_not_void : other /= void; ensure not_void : Result /= void; infix "/" (other : like Current) : REAL -- Division of `Current' by `other' require other_not_void : other /= void; divisible : valid_divisor (other); ensure not_void : Result /= void; infix "^" (exp : INTEGER) : like Current -- Raise `Current' to the `exp'th power require acceptable : (exp >= 0) or else is_invertable; ensure not_void : Result /= void; consistent : (((exp > 0) and then Result.is_equal ((Current ^ (exp - 1)) * Current)) or else ((exp = 0) and then Result.is_equal (one))) or else ((exp < 0) and then Result.is_equal (one / (Current ^ (- exp)))); prefix "-" : like Current -- Unary subtraction applied to `Current' ensure not_void : Result /= void; idempotent : (- Result).is_equal (Current); feature specification valid_divisor (other : like Current) : BOOLEAN -- Can `Current' be divided by `other'? require non_void : other /= void; one : like Current -- The neutral element of multiplication ensure not_void : Result /= void; zero : like Current -- The neutral element of addition ensure not_void : Result /= void; consistent : Result.is_equal (Current - Current); feature specification -- Conversion features to_character : CHARACTER -- Convert `Current' to its equivalent as a CHARACTER. require valid_range : (item >= 0) and (item <= maximum_character_code); to_double : DOUBLE -- Convert `Current' to its equivalent as a DOUBLE. to_real : REAL -- Convert `Current' to its equivalent as a REAL. end interface -- class INTEGER_REF -- Pseudo-class for basic type INTEGER. -- -- Inheritance: -- INTEGER_REF -- export {NONE} make -- end; expanded class interface INTEGER ancestors INTEGER INTEGER_REF COMPARABLE_NUMERIC COMPARABLE PART_COMPARABLE NUMERIC ADDABLE HASHABLE feature summary infix "*" (other : like Current) : like Current prefix "+" : like Current infix "+" (other : like Current) : like Current infix "-" (other : like Current) : like Current prefix "-" : like Current infix "/" (other : like Current) : REAL infix "//" (other : like Current) : like Current infix "<" (other : like Current) : BOOLEAN infix "<=" (other : like Current) : BOOLEAN infix ">" (other : like Current) : BOOLEAN infix ">=" (other : like Current) : BOOLEAN infix "\\" (other : like Current) : like Current infix "^" (exp : INTEGER) : like Current hash_code : INTEGER is_invertible : BOOLEAN item : INTEGER max (other : like Current) : like Current min (other : like Current) : like Current one : like Current relative_to (other : like Current) : INTEGER to_character : CHARACTER to_double : DOUBLE to_real : REAL to_string : STRING valid_divisor (other : like Current) : BOOLEAN zero : like Current inherited features -- From INTEGER_REF: infix "*", infix "+", infix "-", prefix "-", infix "/", infix "//", infix "<", infix "\\", infix "^", hash_code, item, one, to_character, to_double, to_real, to_string, valid_divisor, zero -- From COMPARABLE: infix "<=", max, min, relative_to -- From PART_COMPARABLE: infix ">", infix ">=" -- From NUMERIC: is_invertible -- From ADDABLE: prefix "+" end interface -- class INTEGER -- Pseudo-class for basic type POINTER. -- -- Inheritance: -- POINTER_REF -- export {NONE} make -- end; expanded class interface POINTER ancestors POINTER POINTER_REF feature summary item : POINTER to_string : STRING inherited features -- From POINTER_REF: item, to_string end interface -- class POINTER -- Reference version of the basic type POINTER. -- -- Inheritance: -- -- none class interface POINTER_REF ancestors POINTER_REF feature summary item : POINTER make (p : POINTER) to_string : STRING creation make feature specification make (p : POINTER) -- Make a POINTER_REF from POINTER `p'. ensure item_set : item = p; item : POINTER -- The value of this reference to_string : STRING -- New string containing a printable representation of `item' ensure not_void : Result /= void; end interface -- class POINTER_REF -- Pseudo-class for basic type REAL. -- -- Inheritance: -- REAL_REF -- export {NONE} make -- end; expanded class interface REAL ancestors REAL REAL_REF COMPARABLE_NUMERIC COMPARABLE PART_COMPARABLE NUMERIC ADDABLE feature summary infix "*" (other : like Current) : like Current prefix "+" : like Current infix "+" (other : like Current) : like Current prefix "-" : like Current infix "-" (other : like Current) : like Current infix "/" (other : like Current) : like Current infix "<" (other : like Current) : BOOLEAN infix "<=" (other : like Current) : BOOLEAN infix ">" (other : like Current) : BOOLEAN infix ">=" (other : like Current) : BOOLEAN infix "^" (other : INTEGER) : like Current abs : like Current ceiling : like Current floor : like Current is_invertible : BOOLEAN item : REAL max (other : like Current) : like Current min (other : like Current) : like Current one : like Current power (other : like Current) : like Current relative_to (other : like Current) : INTEGER round : like Current round_to_zero : like Current sign : INTEGER to_double : DOUBLE to_integer : INTEGER to_string : STRING valid_divisor (other : like Current) : BOOLEAN zero : like Current inherited features -- From REAL_REF: infix "*", infix "+", prefix "-", infix "-", infix "/", infix "<", infix "^", abs, ceiling, floor, item, one, power, round, round_to_zero, sign, to_double, to_integer, to_string, valid_divisor, zero -- From COMPARABLE: infix "<=", max, min, relative_to -- From PART_COMPARABLE: infix ">", infix ">=" -- From NUMERIC: is_invertible -- From ADDABLE: prefix "+" end interface -- class REAL -- Reference version of the basic type REAL. -- -- Inheritance: -- COMPARABLE_NUMERIC -- redefine -- to_string, infix "^", infix "-", zero -- end; class interface REAL_REF ancestors REAL_REF COMPARABLE_NUMERIC COMPARABLE PART_COMPARABLE NUMERIC ADDABLE feature summary infix "*" (other : like Current) : like Current prefix "+" : like Current infix "+" (other : like Current) : like Current prefix "-" : like Current infix "-" (other : like Current) : like Current infix "/" (other : like Current) : like Current infix "<" (other : like Current) : BOOLEAN infix "<=" (other : like Current) : BOOLEAN infix ">" (other : like Current) : BOOLEAN infix ">=" (other : like Current) : BOOLEAN infix "^" (other : INTEGER) : like Current abs : like Current ceiling : like Current floor : like Current is_invertible : BOOLEAN item : REAL make (r : REAL) max (other : like Current) : like Current min (other : like Current) : like Current one : like Current power (other : like Current) : like Current relative_to (other : like Current) : INTEGER round : like Current round_to_zero : like Current sign : INTEGER to_double : DOUBLE to_integer : INTEGER to_string : STRING valid_divisor (other : like Current) : BOOLEAN zero : like Current creation make inherited features -- From COMPARABLE: infix "<=", max, min, relative_to -- From PART_COMPARABLE: infix ">", infix ">=" -- From NUMERIC: is_invertible -- From ADDABLE: prefix "+" feature specification item : REAL -- The value of this reference make (r : REAL) -- Make a REAL_REF from REAL `r'. ensure item_set : item = r; to_string : STRING -- New string containing a printable representation of `item' ensure not_void : Result /= void; feature specification -- Power infix "^" (other : INTEGER) : like Current -- Raise `Current' to the power `other'? See `power' below. -- GUSTAVE CATEGORY: CORE(arg,pre,post) -- GUSTAVE Note: The signature of `infix "^"' is different from the one -- listed in ETL. See `power' below. require acceptable : (other >= 0) or else is_invertable; ensure not_void : Result /= void; consistent : (((other > 0) and then Result.is_equal ((Current ^ (other - 1)) * Current)) or else ((other = 0) and then Result.is_equal (one))) or else ((other < 0) and then Result.is_equal (one / (Current ^ (- other)))); power (other : like Current) : like Current -- Raise `Current' to the power `other'? See `infix "^"' above. require positive : item > 0.0; ensure not_void : Result /= void; feature specification -- From COMPARABLE: infix "<" (other : like Current) : BOOLEAN -- Is `Current' less than `other'? require other_not_void : other /= void; ensure other_not_less_or_equal : Result = (not (other <= Current)); consistent : Result implies (not (other <= Current)); not_reflexive : (Current = other) implies (not Result); feature specification -- From NUMERIC: infix "+" (other : like Current) : like Current -- Sum of `Current' and `other' require other_not_void : other /= void; ensure not_void : Result /= void; commutative : Result.is_equal (other + Current); infix "-" (other : like Current) : like Current -- Difference between `Current' and `other' require other_not_void : other /= void; ensure not_void : Result /= void; consistent : Result.is_equal (Current + (- other)); infix "*" (other : like Current) : like Current -- Product of `Current' by `other' require other_not_void : other /= void; ensure not_void : Result /= void; infix "/" (other : like Current) : like Current -- Division of `Current' by `other' require other_not_void : other /= void; divisible : valid_divisor (other); ensure not_void : Result /= void; prefix "-" : like Current -- Unary subtraction applied to `Current' ensure not_void : Result /= void; idempotent : (- Result).is_equal (Current); feature specification valid_divisor (other : like Current) : BOOLEAN -- Can `Current' be divided by `other'? require non_void : other /= void; one : like Current -- The neutral element of multiplication ensure not_void : Result /= void; zero : like Current -- The neutral element of addition ensure not_void : Result /= void; consistent : Result.is_equal (Current - Current); feature specification -- Additional comparison features sign : INTEGER -- Sign of `Current': -- -1 if `Current < zero' -- 0 if `Current = zero' -- 1 if `Current > zero' ensure negative_condition : (Result = (- 1)) = (Current < zero); zero_condition : (Result = 0) = (not ((Current < zero) or (Current > zero))); positive_condition : (Result = 1) = (Current > zero); abs : like Current -- The absolute value of `Current' ensure not_void : Result /= void; same_as_negative : (Current < zero) = (relative_to (- Result) = 0); same_if_positive : (Current >= zero) = (relative_to (Result) = 0); feature specification -- Conversion features to_double : DOUBLE -- Convert `Current' to its equivalent as a DOUBLE. to_integer : INTEGER -- Convert `Current' to an integer, discarding the any non-integral -- portion of `Current's value (ie., truncate). To control the -- truncation behavior, use in conjunction with `floor', `ceiling', -- `round' or `round_to_zero' (e.g., `value.round.to_integer'). floor : like Current -- The greatest integral value less than or equal to `Current' ensure not_void : Result /= void; ceiling : like Current -- The least integral value greater than or equal to `Current' ensure not_void : Result /= void; round : like Current -- The rounded integral value of `Current'. If `Current = 0.5', -- returns `ceiling'. ensure not_void : Result /= void; round_to_zero : like Current -- The rounded integral value of `Current'. If `Current = 0.5', -- returns `floor'. ensure not_void : Result /= void; end interface -- class REAL_REF ================================================== End of NICE-ESG-Libs Digest ******************************