NetNews Usenet Archive 1993 #3/NN_1993_3.iso/spool/comp/lang/eiffel/1445

Text File | 1993-01-21 | 3.4 KB | 97 lines

Path: sparky!uunet!mcsun!uknet!mucs!cs.man.ac.uk!mod
From: [e-mail] (Mike O'Docherty (Teaching Company Associate))
Newsgroups: comp.lang.eiffel
Subject: Re: creation
Message-ID: <[e-mail]>
Date: 21 Jan 93 10:15:37 GMT
References: <[e-mail]>
Sender: [e-mail]
Lines: 86

[e-mail] (William Stuart-smith) writes:

>[e-mail] (Mike O'Docherty (Teaching Company Associate))
>writes
>> On page 128 of "Eiffel: The Language", it is stated (in the definition of
>> consistency) that postconditions need not be checked on return from a
>> creation procedure. I see no reason why they they should be let off the
>> hook; is this a mistake?

>It seems correct to me. A creation procedure sets up the invariant of its
>class: It returns nothing and affects only its class, therefore the only
>'postcondition' (in the sense of the entire condition which is implied by the
>precondition for correctness) that applies pertains to the state of the class
>as a whole and is therefore the invariant.

>Where do you suggest that this would be insufficient, and what 'require'
>clause would you add?

class X
creation
    make
feature
    identity: STRING;

    make(id: STRING) is
        require
            valid_id: id /= Void and then id.count /= 0
        do
            identity := clone(id);
        ensure
            id_set: equal(identity, id)
        end
end -- class X

The next time assertion checking is spelled out is on page 133. Here it is
stated that "The implementation should enable developers to set various
evaluation levels for assertions. ... The possible levels ... are" followed
by a list. Two points in this list worry me:

    . ensure: also evaluate postconditions on return from routines of this class

[This contradicts the statement on page 128 since a creation procedure is a
routine]

    . invariant: also evaluate the class invariant on entry to and return
      from qualified calls to routines of [this class]

[Now, you'd better not check the invariant on entry to a routine if it happens
to be a creation procedure called by a creation instruction, otherwise

class Y
creation
    make
feature
    identity: STRING;
feature {NONE}
    make(id: STRING) is
        do
            identity := clone(id);
        end
invariant
    valid_id: identity /= Void and then identity.count /= 0
end -- class Y

will never run with assertions switched on --- on entry to make, the
`identity /= Void'  part of the invariant is bound to fail!
]

Some clarification/correction is called for in this Chapter. The fact that
`creation procedure' is ambiguous doesn't help --- is it "a routine exported for
use in a creation instruction (and perhaps also for use as a simple procedure"
or "a procedure *being used* to execute a
creation instruction".

Sorry, I didn't intend this to turn into a critique of / erratum for ETL, but
I was compiling some code and this chapter had me scratching my head for quite
a while.

Mike.

-------------------------------------------------------------------------
"Lou Reed was singing about scoring drugs. Tom Robinson was singing about
scoring sex. I don't know what she's singing about, Dolly Mixtures
probably." --- Nicky Campbell on Vanessa Paradis' cover of "Waiting for
the man"   => => => => => => => => => => => => => => =>  [e-mail]
-------------------------------------------------------------------------