🚀 go-pugleaf

From <1799@novavax.UUCP> by weiner@novavax.UUCP (Bob Weiner):

> Rather than sprinkle pre- and post-conditions around routines that say:
> 
>     require
>        param > 0
> 
> and other such things, it makes sense to create classes for POS_INT,
> NON_NEG_INT and so forth and then type the formal parameters of the
> routines.
> 
> I do hope that Eiffel V3.0 will correct this limitation.  Even better, I
> would enjoy finding out that I am mistaken in my view.

    I agree that it should be possible for programmers to define such
classes by inheriting from INT and adding the proper invariants.
This is an implementation problem and I have had good hope that we
(or others) will be able to solve it.

    Assuming this is the case, however, I am not so sure that
these classes should be added to the Kernel Library. This is because
I have some doubts about their practical applicability.
(This should be taken literally: at this point I am neither for or against
their inclusion in version 3, just doubtful.) The problem is that
POS_INT, NON_NEG_INT etc. are not *closed* for the arithmetic operations.
For example, with

    p1, p2: POS_INT;
    n1, n2: NEG_INT

there is no guarantee that p1 - p2 will be a POS_INT or that n1 - n2 will
be a NEG_INT. The best information we can deduce (the ``and'' in the
lattice of types) is just INT.

Similarly, if we define interval types of the form

    class INTERVAL export
        repeat INT, low, high
    inherit
        INT
    feature
        low, high: INTEGER;

        Create (a, b: INTEGER) is
                -- Set interval bounds to `a' and `b'.
            do
                low := a; high := b
            end; -- Create

    invariant
        value >= low; value <= high
    end -- class INTERVAL

they will not help us very much since for n of type INTERVAL we
have no static way of determining whether n + 1 is still
compatible.

    In all these cases we will have to resort to assertions anyway.

    All this is not surprising. We should not hope that a
static type system will magically solve problems that are
fundamentally dynamic in nature.

    The problem is not essentially different from the situation with
interval types in Pascal, as analyzed by A. Nico Habermann
(``Critical Comments on the Programming Language Pascal'',
Acta Informatica, 3, 1973, pages 47-57).

    The above is not a contention that Mr. Weiner is ``mistaken
in his view''. Simply, I am not convinced that the suggested classes
will solve more problems than they raise.

-- Bertrand Meyer
bertrand@eiffel.com