[comp.lang.eiffel] assertions on deferred features

giacomet@venus.ecn.purdue.edu (Frederic B Giacometti) (09/07/90)

A question concerning deferred features and their assertions in the ISE
implementation of the language:
   Pre and post conditions (require and insure assertions)
associated to the definition of deferred features do not appear
on the "flat" version of the descendent effective classes. So my
question is:
   Are assertions associated with deferred definitions
inforced by the language implementation (and then there's a bogus
in the flat program), or do I have to restate them myself in the
effective definition (and then the implementation has a bogus) ? 


Thanks,

Frederic Giacometti
School of Industrial Engineering
Purdue University

rick@tetrauk.UUCP (Rick Jones) (09/10/90)

In article <1990Sep6.184123.22260@ecn.purdue.edu> giacomet@venus.ecn.purdue.edu (Frederic B Giacometti) writes:
>A question concerning deferred features and their assertions in the ISE
>implementation of the language:
>   Pre and post conditions (require and insure assertions)
>associated to the definition of deferred features do not appear
>on the "flat" version of the descendent effective classes. So my
>question is:
>   Are assertions associated with deferred definitions
>inforced by the language implementation (and then there's a bogus
>in the flat program), or do I have to restate them myself in the
>effective definition (and then the implementation has a bogus) ? 

The current compiler does not automatically inherit pre- & post- conditions for
you, either from deferred routines, or implemented routines which you re-define,
although it does force inheritance of the invariant.  I did query this once
with ISE, and it is not as simple as it sounds.

The problem is that in your new feature, you may want to modify these
conditions.  Not only that, but if you do, a different post-condition should be
TIGHTER than the inherited one, while a different pre-condition should be
LOOSER.  The theory of this is in Bertrand Meyer's "OOSC" book.  While not
impossible to implement, I get the impression that ISE decided it was
sufficiently difficult and/or would give rise to such efficiency problems that
it was omitted.  The principle is that you are supposed to read the pre- &
post- conditions of what you are inheriting from, and re-state the same or
suitably modified versions in your routine.

Given that this is how you are supposed to use the language, I would say that
the main problem is that it doesn't seem to be clearly explained anywhere in
the manuals.  I also have some recollection that this problem was going to be
addressed in a future version of the compiler.  Can anyone at ISE comment?

-- 
Rick Jones			Nothing ever happens, nothing happens at all
Tetra Ltd.			The needle returns to the start of the song
Maidenhead, Berks, UK		And we all sing along like before
rick@tetrauk.uucp						- Del Amitri