🚀 go-pugleaf

bertrand@eiffel.com (Bertrand Meyer) writes:

>From <mod.727464101@cs.man.ac.uk> by mod@cs.man.ac.uk
>(Mike O'Docherty (Teaching Company Associate)):

>> 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?

>Actually the extract does not address what should be checked.
>It defines class consistency, which is a static
>(i.e. mathematical) concept.

Point taken. Ok, I'll have to plead ignorance on the *true* meaning of Section
9.1.2., but it still seems to me that condition 1 should be

        {pre } do  {post  ^  INV }
            p    p      p       C

>The discussion of run-time assertion monitoring on page 133
>does say what should be checked at run time, and makes no
>distinction between creation procedures and other routines.

My point is that it *should* make a distinction, because you *shouldn't* check
invariants on entry to creation procedures *when they are called from a
creation instruction*.

Maybe I can stop this going any further by summarising the run-time situation
with assertions switched on, as described by Raphael Manfredi in his message
(for the benefit of anyone else confused so far :-) )

1) Invariants are checked on entry to *every* routine *unless*
    a) That routine is a creation procedure *called from a creation
       instruction*.
    b) that routine call is local (ie. an object calls one of its own
       routines).
2) Invariants are checked on exit from *every* remote routine call (ie. an
   object's routine called by another object).
3) Preconditions are checked on entry to *every* routine.
4) Postconditions are checked on exit from *every* routine.

I can't speak for loop variants, loop invariants or check instructions because
I haven't used them (so shoot me :-) ).

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"   => => => => => => => => => => => => => => =>  mod@cs.man.ac.uk
-------------------------------------------------------------------------