Path: utzoo!attcan!uunet!know!sdd.hp.com!ucsd!hub.ucsb.edu!eiffel!bertrand
From: bertrand@eiffel.UUCP (Bertrand Meyer)
Newsgroups: comp.lang.eiffel
Subject: Re: Assertions and deferred routines
Message-ID: <420@eiffel.UUCP>
Date: 18 Oct 90 15:02:19 GMT
References: <443@kepler1.kepler.com>
Organization: Interactive Software Engineering, Santa Barbara CA
Lines: 79


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