Path: utzoo!attcan!uunet!midway!ncar!asuvax!cs.utexas.edu!usc!ucsd!hub.ucsb.edu!eiffel!bertrand
From: bertrand@eiffel.UUCP (Bertrand Meyer)
Newsgroups: comp.lang.eiffel
Subject: Re: Assertions and deferred routines
Message-ID: <425@eiffel.UUCP>
Date: 22 Oct 90 05:13:56 GMT
References: <443@kepler1.kepler.com> <420@eiffel.UUCP> <7185.2721e72b@swift.cs.tcd.ie>
Organization: Interactive Software Engineering, Santa Barbara CA
Lines: 70

In <7185.2721e72b@swift.cs.tcd.ie>, cjmchale@swift.cs.tcd.ie
(Ciaran McHale) questions the Eiffel 3 rule for changing the
assertions of redeclared routines (``require else'' and
``ensure then'').  Of his (?) two objections, I believe
the second one is more justified than the first.

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

	This is a general feature of inheritance, not a problem specific
to assertions. You cannot understand a class fully without its
ancestry.

	In Eiffel, however, the problem has a simple solution: flat.
The documentation for a class is produced by the ``flat'' tool which
reconstructs an inheritance-free version of a class, with every
inherited feature copied from the appropriate ancestor; renaming and
redefinition are of course taken into account, and the class
invariant is expanded so as to accumulate all ancestors' invariant
clauses. This (is combination with ``short'', the interface
abstracter) is how class documentation is routinely produced.

	An obvious consequence of the new rules for assertions of
redeclared routines is that the flat form of a class including
redeclared routines with new assertions will automatically include
the expanded form (with or-elses applied to preconditions and and-thens
applied to postcondition), so that programmer reading about a class
(through the flat or flat-short form) will see the actual assertions
without having to look at ancestors. (This was mentioned in the
original posting on this problem <229@eiffel.UUCP> of January 1990,
but I forgot to repeat it in my recent response to Frank Caggiano
<443@kepler1.kepler.com>.)

	Interactive browsing tools should perform similar expansions.

> 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 [routine] 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'>

Yes, this is true. For example a postcondition that reads x > 5
may be strengthened by ``ensure then x > 10''. The result,
as expanded by flat, and implemented if assertion monitoring
is turned on, will read

/1/
	x > 10 and then x > 5

It is not unconceivable that a compiler writer could use or write
a simple symbolic manipulation package for boolean algebra to simplify
such expanded assertions, at least in straightforward cases such
as this one.

	Even without this, however, the problem does not seem
to have disastrous consequences. Note that it already exists
today, in the case of invariants: class A can have x > 5 as one of
its invariant clauses, and B, a descendant of A, can add x > 10.
Then the expanded invariant is /1/ above. This is unpleasant,
but does not seem to have caused major problems.
-- 
-- Bertrand Meyer
bertrand@eiffel.com