[comp.lang.eiffel] Assertions and deferred routines

fcaggian@kepler.com (Frank Caggiano) (10/18/90)

According to both 'Eiffel: The language' and 'Object-oriented
Software Costruction'  pre and post conditions from deferred 
routines should be in force in any descendants.  I take this
to mean that if a deferred routine has a `require' statement
then the conditions in the statement are enforced in the 
descendents WITHOUT having to explicitly re-write the 
statements.

Is this in fact true?  I still am running 2.2 B (waiting quietly
for 2.3 ) and it appears not to be the case.

Does anyone know if this is a know bug, am I misreading the 
book or am I doing something wrong.  and if it is a bug is
it fixed in 2.3 (and when will 2.3 be released).

Here is an example of the code:
--------------------------------------------------------------------------
--  Copyright (C) Kepler Financial Mgmt.				--
--  100 North Country Rd., Setauket NY, 11733				--
--									--
-- Frank Caggiano							--
-- Thu Oct 11 10:54:20 EDT 1990						--
--------------------------------------------------------------------------
--
-- General notion of displaying a figure in  X
--
deferred class XDISPLAY_FUNCTION export
	
	display, erase

feature

	display (fig_ref: GEN_FIGURE; w: WINDOW) is
			-- Display figure in window
		require
			have_figure: not fig_ref.void;
			window_exists: not w.void;
		deferred
		end; -- display


	erase (fig_ref: GEN_FIGURE; w: WINDOW) is
			-- Erase figure from window
		require
			have_figure: not fig_ref.void;
			window_exists: not w.void;
		deferred
		end; -- erase

end; -- class XDISPLAY_FUNCTION

In this class the assertion check does not happen unless I explicitly
write out the require statement in the routine definantion.


--------------------------------------------------------------------------
--  Copyright (C) Kepler Financial Mgmt.				--
--  100 North Country Rd., Setauket NY, 11733				--
--									--
-- Frank Caggiano							--
-- Thu Oct 11 10:54:20 EDT 1990						--
--------------------------------------------------------------------------
--
--  class to draw an ellipse in X
--
class X_DRAW_ELLIPSE export
		
	display, erase

inherit

	XDISPLAY_FUNCTION
		define
			display,erase
feature

	display (fig_ref: ELLIPSE; w: GRAPH_WINDOW) is
		external
			ellipse_draw language "C"
		do
			fig_ref.xgc.set_gc;

			ellipse_draw(w.imp_reference, fig_ref.xgc.imp_ref,
					fig_ref.origin.winx(w), fig_ref.origin.winy(w),
					(fig_ref.int_major_axis * w.draw_num) div w.draw_denom,
					(fig_ref.int_minor_axis * w.draw_num) div w.draw_denom);
				
		end;

	erase (fig_ref: ELLIPSE; w: GRAPH_WINDOW) is
		-- Erase ellipse from 'w'. 
		-- NOTE: this is NOT a 'rubberband' type of erase. 
		-- See class RUBBER and its desendents. 
		external 
			ellipse_draw language "C" 
		local
			gc: GRAPHIC_IMP
		do 
			gc.create;
			gc.set_background_by_pixel(w.back_color);
			gc.set_foreground_by_pixel(w.back_color);
			gc.set_gc;

			ellipse_draw(w.imp_reference, gc.imp_ref,
					fig_ref.origin.winx(w), fig_ref.origin.winy(w),
					(fig_ref.int_major_axis * w.draw_num) div w.draw_denom,
					(fig_ref.int_minor_axis * w.draw_num) div w.draw_denom);

		end; -- erase
end;
-- 
Frank Caggiano                      INTERNET: fcaggian@kepler.com  
Kepler Financial Management, Ltd.       UUCP: ..!uunet!kepler1!fcaggian
100 North Country Rd.                    fax: (516) 751-8678
Sekauket, NY 11733                     voice: (516) 689-6300 

bertrand@eiffel.UUCP (Bertrand Meyer) (10/18/90)

The point raised by Mr. Caggiano was discussed in detail last
January; see my posting <229@eiffel.UUCP> dated 18 January 90
and entitled ``A planned change for assertions applying to
redefined routines'', with a response by Alonzo Gariepy
from Microsoft (<10366@microsoft.UUCP>).

The language rules are that preconditions may be weakened and
postconditions strengthened. However, as explained quite
precisely (I hope) in ``Object-Oriented Software Construction''
(11.1.3, page 258), the rules are not enforced by the current
language definition, so that assertions have to be repeated even if
they have not changed.

This was a language problem, not an implementation bug.

The reason for this problem is simply that I had not seen
at the time of the original design the proper (and a posteriori
rather obvious) solution, which will be part of Version 3 (not 2.3).

To summarize the new syntax and semantics (see the January posting
for more detail):

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.
(In an intermediate release they will probably
give rise only to a compiler's warning message, so as
not to break existing code.) 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''

thus enforcing the weakening/strengthening postcondition
automatically, since by the laws of Boolean algebra

	a implies (a or b)

	(a and b) implies a

regardless of what b is. (The syntax used in the January posting
was `require or' and `ensure and'; the modification is cosmetic,
for consistency with other parts of the language.) 

One important advantage of this change, which directly addresses
Mr. Caggiano's comment, appears in the frequent case in which the
assertions do not change. The simple convention is that an absent
`require else' clause is equivalent to

	require else false

and an absent `ensure then' clause is equivalent to

	ensure then true

which means keeping the old assertions since by Boolean algebra

	a or false = a
	a and true = a

so that in many cases it will indeed be possible simply to omit
the precondition and/or postcondition of a redeclared feature,
thus keeping the old versions. 
-- 
-- Bertrand Meyer
bertrand@eiffel.com

fcaggian@kepler.com (Frank Caggiano) (10/19/90)

Thanks to all for clearing up this problem.  I was lead astray
by Section 10.3.4 'Specifying the semantics of deferred routines'
in the Book.  Starting at the bottom of page 236 with the
paragraoh begining 'Only with assertions do deferred classes attain
their full power. ... '.  This paragraph in particular seems to
imply that assertions hold for actual implementaions of deferred
routines.  In fact further on in the paragraph it is written,
'all variants of push in descendents of STACK are constrained
by the above specification.'  I was further confused by the 
nomenclature used.  Pages 256 seemed to deal with redefinition
and I was under the impression that creating an efective 
instance of a deferred routine was definition. This confusion
arose from page 48 of 'Eiffel: The language' bottom of the page
'DEFINITION: defining a feature' which uses the keyword 'define'
which isn't even mentioned (as far as I can tell) in the Book.
(see also page 39 of 'Eiffel: The language' section 7.7 4th
bullet item).  

	Anyway this could probably go on for quit a while more
and not accomplish much else. One thing I feel would help 
avoid these misunderstandings would be more timely output from
ISE. What I mean by this is a compilation of issues, know bugs
etc. To both of my last postings I was told that what I was
asking had been mentioned in a previous posting. (Dr. Meyer refered
me back to a posting in January of this year) Does ISE have
an archive of this group that is avaliable?  As we only received
Eiffel in May of this year I wasn't reading the group back in Jan.
(in fact I was gainfully unemployed in Jan, not reading any 
netnews). In fact looking at what I just wrote it really doesn;t 
matter if ISE has the archive or not. As a customer of ISE I 
expect to be informed of these issues directly. This especially
applies to know problems in the documentaion. 

	Bugs in both the documentation and software are, and were,
expected in a new product such as this. We are willing to put up
with them because the rest of the system offers so much in the way
of software construction it leaves most other technologies far
behind.  What is harder to put up with is re-inventing the wheel.
If I have to discover for myself all the issues which were 
discussed a year ago the productivity gains are lost.

	I offer these comments as one who has become hooked on
Object Oriented programing in general and Eiffel in particular and
would hate to see ISE shoot itself in the foot. How many other
products have been lost to human-kind through the centuries because
the implementation did not live up to the idea and the custommers
got tired of waiting . I mean do we really want our grandchildren 
programming in C++*2 :-) .

			Frank Caggiano

-- 
Frank Caggiano                      INTERNET: fcaggian@kepler.com  
Kepler Financial Management, Ltd.       UUCP: ..!uunet!kepler1!fcaggian
100 North Country Rd.                    fax: (516) 751-8678
Sekauket, NY 11733                     voice: (516) 689-6300 

bertrand@eiffel.UUCP (Bertrand Meyer) (10/20/90)

From <445@kepler1.kepler.com> by fcaggian@kepler.com (Frank Caggiano):

> Thanks to all for clearing up this problem.  I was lead astray
> by [various incomplete or ambiguous statements in
> ``Object-Oriented Software Construction''].

Thanks for this precise list. It will certainly be put to good
use for the second edition (if and when...).

> To both of my last postings I was told that what I was
> asking had been mentioned in a previous posting. (Dr. Meyer refered
> me back to a posting in January of this year)
> [...]
> As we only received
> Eiffel in May of this year I wasn't reading the group back in Jan.

	By mentioning previous postings I certainly did not intend
to dismiss the questions raised by Mr. Caggiano or to give the
impression that they were irrelevant. It is perfectly natural that
certain questions should recur as new users join the discussion.
The sequence of events may then be the following: someone raises
a question that has already been discussed (although perhaps in
somewhat different terms); someone else (me in the case under
review) responds with a message giving the references to the earlier
discussion, and summarizing their main points. This gives both an
immediate answer, and a pointer to more exhaustive articles.
This seems to be the right way to work.

> 	I offer these comments as one who has become hooked on
> Object Oriented programing in general and Eiffel in particular and
> would hate to see ISE shoot itself in the foot.
> [...] 
> Does ISE have an archive of this group that is available?

Now here is an opportunity to shoot myself in the remaining foot.
The answer is (sorry) that the question was dealt with
in a previous posting. There is an archive, courtesy of
Digital Equipment's Western Research Lab, and thanks to the
efforts of Roger H. Goun. Quoting from his message
<14686@shlump.nac.dec.com> of August 18, 1990:

|| I'm pleased to announce that an archive of the comp.lang.eiffel
|| newsgroup is now available on gatekeeper.dec.com.

|| The files are in /pub/plan/eiffel/usenet/USENET-xx-yyy, where `xx'
|| represents the last two digits of the year and `yyy' the month of
|| posting. Compressed versions of the files are also available.
|| 
|| From IP (either inside DEC or outside DEC):
||     anonymous FTP to gatekeeper.dec.com (16.1.0.2)
||     cd pub/plan/eiffel/usenet
||     get USENET-xx-yyy (or to get the compressed copy, bin, get
|| USENET-xx-yyy.Z)
|| 
|| From a UUCP neighbor of decwrl: 
||     "uucp decwrl!~/pub/plan/eiffel/usenet/USENET-xx-yyy.Z"
|| 
|| From the DEC Easynet:
||     DECWRL::"/pub/plan/eiffel/usenet/USENET-xx-yyy"  

(The rest of Mr. Goun's message contained size measurements,
a mention of five apparently missing articles, and acknowledgments.
His mail address is goun@ddif.enet.dec.com.)

> As a customer of ISE I 
> expect to be informed of these issues directly.

	That is a fair expectation. There have not been any
issues of the Eiffel newsletter (Champ-de-Mars) recently and I
apologize for that. The newsletter is being revived.

	On the other hand the newsgroup is a very convenient way of
sharing information with users. Even with a newsletter, or
some other medium, it is still easy for someone (newcomer or not)
to miss a previously published answer. And the newsletter
does not allow one to correct the situation by posting a public
request.

> How many other
> products have been lost to human-kind through the centuries because
> the implementation did not live up to the idea and the customers
> got tired of waiting . I mean do we really want our grandchildren 
> programming in C++*2 :-) .

I absolutely agree. The C++ customers will someday get tired of
waiting. Actually there was a posting on this theme recently in the
C++ newsgroup on precisely this theme (I have no remaining foot
to shoot, but for the record the reference is <752@ubbpc.UUCP>,
by William G. Hutchison of Unisys): ``Waiting for
Godot'' to bring exceptions, genericity and other minor amenities.
As for our grandchildren, only the paleontology professors
among them will know what C++ was.

-- Bertrand Meyer
bertrand@eiffel.com

cjmchale@swift.cs.tcd.ie (10/22/90)

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.

bertrand@eiffel.UUCP (Bertrand Meyer) (10/22/90)

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

richieb@bony1.uucp (Richard Bielak) (10/22/90)

In article <7185.2721e72b@swift.cs.tcd.ie> cjmchale@swift.cs.tcd.ie writes:

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

In Eiffel you can simply use the "flat" utility (or flat | short)
to see the complete specification of a class including the
appropriate pre-conditions from all the parents.


...richie



-- 
+----------------------------------------------------------------------------+
|| Richie Bielak  (212)-815-3072      |  If a thousand people say a foolish  |
|| USENET:        richieb@bony.com    |  thing, it's still a foolish thing.  |
+----------------------------------------------------------------------------+

schaerer@gorgo.ifi.unizh.ch (10/23/90)

[Bertrand Meyer announces that Eiffel 3.0 will offer the syntax "require
 else ..." and "ensure then ..." for pre/postconditions in redeclarations]

I have a cosmetic problem with the proposed syntax. Although you give a
logically consistent explanation for it, I think it is not very readable
for humans, a very important aspect in language design in my opinion.
I'd rather like to see something verbose like

     alternatively require ``additional precondition''

     additionally ensure ``additional postcondition''
 
Did you ever consider any proposal along these lines?
---
Daniel Schaerer, University of Zurich/Switzerland
schaerer@ifi.unizh.ch

bertrand@eiffel.UUCP (Bertrand Meyer) (10/24/90)

From <1990Oct22.181347.6410@gorgo.ifi.unizh.ch> by
schaerer@gorgo.ifi.unizh.ch (Daniel Schaerer):

> I have a cosmetic problem with the proposed syntax
> ["require >  else ..." and "ensure then ..."].
> [...] I think it is not very readable
> for humans, a very important aspect in language design in my opinion.
> I'd rather like to see something verbose like
> 
>      alternatively require ``additional precondition''
> 
>      additionally ensure ``additional postcondition''
>  
> Did you ever consider any proposal along these lines?

	All Eiffel keywords are simple English words. I would personally be
somewhat uncomfortable with a keyword such as ``additionally'',
given the probability of misspelling. (Considering the possibility
of using one `d', two `t', two `n' or one `l', this gives 15
possible misspellings for non-native speakers, bad spellers, or careless
typists!)

	It is certainly true that readability is an important criterion,
but it is not the same thing as verbosity. In particular, mimicking
natural language is not a solution: programming languages are very
simple codes, quite far from the complexity and wealth of expression of
English or another natural language. We want their syntactic structure
to reflect this simplicity; on the other hand, we do want
programming languages to be reminiscent of natural language,
hence the use of English words as keywords and other conventions
borrowed from human language. These two criteria are somewhat
contradictory; if you focus on just one of them, you get at
one end APL and at the other Cobol. The concrete syntax of
most programming languages is in-between. I cannot guarantee that
the Eiffel solution is perfect, but I can claim that the
design choices were made carefully and consciously.

	For a programming language, I would take ``readability'' from the
viewpoint not of an arbitrary reader but of one who has a basic
knowledge of the language. If person X, who does not know Eiffel,
looks at an Eiffel class text and cannot understand what a ``require
else'' clause stands for, this is regrettable, but not a tragedy.
The more important questions relate to users Y, who has taken a couple
of hours to read an introduction to Eiffel, and Z, who is a frequent
Eiffel user. The questions are:

	- Assuming Y has read the few lines about precondition weakening
	and postcondition strengthening, will he remember the convention
	right away when he comes across a ``require else'' in an existing
	class?

	- Will Z learn quickly the convention and be able to apply it
	frequently without hesitation (that is to say, without going back
	to the language manual)?

I hope the answer to both questions will be yes.

	Once the language designer begins to consider that his immediate
constituency is Y and Z more than X (although X is not to be neglected,
of course, since we do want to turn him soon into a Y or Z),
then ``verbosity'' yields to criteria such as regularity and consistency.
To take a cosmetic example from another part of the language,
a ``microscopic'' view of readability would suggest that
a Feature_clause be introduced by the keyword `features' since it can
declare an arbitrary number of features. Instead, the keyword is `feature',
in keeping with a general Eiffel convention according to which
all nouns used as keywords are in the singular. Here the more
macroscopic criterion is regularity. This is very close to
the criteria used in user interface design: more important than
local perfection is global consistency, the ``principle of least
surprise''.

	All this is probably overkill in response to a comment that
his author described as cosmetic. I won't fight for the ``require else''
and ``ensure then''; they are the best solution I could find
after looking at a number of alternatives. When all arguments have
been made, the final choice of concrete syntax is, to a point,
a matter of taste.
-- 
-- Bertrand Meyer
bertrand@eiffel.com

schaerer@ifi.unizh.ch (*) (10/27/90)

[In a previous posting, I suggested to replace "require else ..." and
 "ensure then ..." by something more readable for humans, and proposed
 "alternatively require ..." and "additionally ensure ...".]
 
[Bertrand Meyer then answered:]

>I would personally be somewhat uncomfortable with a keyword such as
>``additionally'', given the probability of misspelling.

Agreed. I'm just brainstorming. Those two keywords happened to express
exactly what I wanted, but they are somewhat ugly.

>It is certainly true that readability is an important criterion, but it
>is not the same thing as verbosity.

I chose the wrong word when I asked for "something verbose", I should have
asked for "something structurally closer to natural language" instead.

>[long discussion of readability issues]
>
>All this is probably overkill in response to a comment that his author
>described as cosmetic.

I usually enjoy your verbose (:-) and thoughtful postings -- count me as one
of your admirors.

Two more proposals:

  else require ...         then ensure ...         (conjunction precedes verb)
                                                   (parsing problems with am-
                                                    biguous use of then/else?)

  require again else ...   ensure again then ...   (this one *is* verbose...)

---
Daniel Schaerer, University of Zurich/Switzerland