Path: utzoo!attcan!uunet!mcsun!ukc!tcdcs!swift.cs.tcd.ie!cjmchale
From: cjmchale@swift.cs.tcd.ie
Newsgroups: comp.lang.eiffel
Subject: Re: Assertions and deferred routines
Message-ID: <7185.2721e72b@swift.cs.tcd.ie>
Date: 21 Oct 90 18:21:31 GMT
References: <443@kepler1.kepler.com> <420@eiffel.UUCP>
Organization: Computer Science Department, Trinity College Dublin
Lines: 66

In article <420@eiffel.UUCP>, bertrand@eiffel.UUCP (Bertrand Meyer) writes:
> [A new feature to appear in Eiffel 3.0]
> In a redeclaration of a feature (i.e. redefinition,
> or effective declaration of a previously deferred feature),
> the forms using just ``require'' and ``ensure'' will be
> prohibited since they make it impossible to enforce the rules.
> [...] Precondition and postcondition
> clauses for a redeclared feature should instead be of the
> respective forms
> 
> 	require else
> 		``additional precondition''
> 
> 	ensure then
> 		``additional postcondition'''
> 
> The semantics of these constructs is to yield as new
> precondition and postcondition for the redeclared feature:
> 
> 	``old precondition'' or else ``additional precondition''
> 
> 	``old postcondition'' and then ``additional postcondition''

This enforces the weakening/strengthening of pre/postconditions in a
hierarchy. But suppose the hierarchy is quite deep. The programmer
must look up the entire hierarchy for all the components of the
pre/postconditions. Does anybody see this as potentially being
pain in the neck? (I'm _not_ flaming the proposal, I'm just wondering
about the potential drawbacks of it.) I see two potential problems:

1. If somebody wants the full pre/postcondition then he must search
the ancestors of the class for each component. In other words, the
full pre/postcondition is not visible by inspection of the class.

2. The resultant condition might be difficult to understand
since it may be in an expanded form. For instance, suppose the class
hierarchy is: A is the base class, B is derived from A, C is derived
from B. A precondition on a method in class C is of the form:

	<condition 1> or <condition 2> or <condition 3>

It is entirely possible that this compound condition might be
compactable to something more readable to give

	<condition 3'>

which is more compact but equivalent. The more readable the
pre/postconditions, the better documentation they are.
(To the best of my knowledge, at the current state of the art it is
infeasible to make the compiler check the equivalence of conditions.)


Has anybody any thoughts on this matter? Does anybody know from
experience if these potential problems aren't really peoblems in
practice. Followups or email (I'll summarise any email I get) will
be fine by me.


Thanks in advance,
Ciaran.
-- 
Ciaran McHale		"An inappropiate joke for every occasion"
Department of Computer Science, Trinity College, Dublin 2, Ireland.
Telephone: +353-1-772941 ext 1538    FAX: +353-1-772204   Telex: 93782 TCD EI
email: cjmchale@cs.tcd.ie	or	cjmchale%cs.tcd.ie@cunyvm.cuny.edu
	My opinions are.