bertrand@eiffel.UUCP (Bertrand Meyer) (01/18/90)
A planned change for assertions applying to redefined routines
--------------------------------------------------------------
This is the third of a sequence of postings describing the
changes planned for version 3 of Eiffel.
These are cleanup changes and do not affect anything fundamental.
----------------------------------------------------------------------
|WARNING: The change described here is planned for version 3 of the |
|environment, not to be released until late 1990. |
| |
|Any change in the language supported by Interactive's tools |
|will be accompanied by CONVERSION TOOLS to translate ``old'' syntax |
|into new. Programmers will NOT need to perform any significant work |
|to update existing Eiffel software. |
| |
|This posting is made solely for the purpose of informing the Eiffel |
|community about ongoing developments. Although the posting has been |
|preceded by careful reflection and internal discussions within |
|Interactive, and many users of the language and environment, |
|we make no commitment at this point that the features |
|described here will actually be included, and, if they are, that |
|their final form will be the exact one shown below. |
----------------------------------------------------------------------
Background
----------
The use of assertions is one of the most important aspects of Eiffel
programming. Assertions provide indispensable support for specification,
design, documentation and testing of classes.
The very concept of reusability in software does not make sense
without assertions.
Assertions in Eiffel are the manifestation of the underlying theory
of software construction, known as ``programming as contracting'':
building software elements as implementations of precise
interface specifications viewed as contracts between client and
supplier.
Assertions and the notion of programming as contracting combine
particularly well with inheritance. One of the important principles,
described in detail in several of my publications, is that a
redefinition for a routine (meant for dynamic binding) may weaken
the precondition and may strengthen the postcondition.
Another important aspect of assertions, perhaps even more closely
tied to the object-oriented method, is their use as class invariants.
However this part of the mechanism is fine as it is now, so it will
not be discussed further.
Eiffel assertions, although simple and easily understood by programmers
with little mathematical background, constitute of the few wide-scale
and ``real-world'' applications of work on formal specification and
verification.
Purpose of the change.
----------------------
The purpose of the change is to solve two problems at once through
an improved syntax and semantics for the preconditions and postconditions
associated with redefined routines.
Problem 1: As indicated in the book ``Object-Oriented Software
Construction'' and the current Eiffel documentation (especially
``Eiffel: The Language''), the above rule (weakening preconditions/
strengthening postconditions) is only a methodological guideline.
When assertion checking is enabled (for purpose of monitoring
execution, debugging, testing etc.), no check is made that the
precondition of a routine is indeed weaker than the original,
and symmetrically for postconditions.
I won't go into the details of why this is so in current Eiffel but
the situation is regrettable. Methodological guidelines are nice,
but language-supported rules are much better.
Problem 2: Because the methodological principles are not enforced, the
text of a redefined routine does not by itself indicate that the
original precondition/postcondition are still there,
possibly in weakened/strengthened form. In the common case
where the pre and post have not changed, the programmer must
repeat them manually. This is somewhat of a nuisance.
The language change
-------------------
Assume class B inheriting from A, redefining its routine r.
A r (...) is
require
^ P
| do
| ...
| ensure
| Q
|
B inherit A redefine r
feature
r is ...
It is no longer permitted to write the redefined version of r in B
under the form
[1]
r is
require
...
do ...
ensure
...
if, as here, r is a redefined routine. The compulsory form in this case
is
[2]
r is
require or
NP
do ...
ensure and
NQ
which means that the actual precondition and postcondition of the
redefined routine are respectively
P or NP
Q or NQ
so that the principles are automatically enforced: precondition weaker or
equal, postcondition stronger or equal. Run-time monitoring, if
enabled, will apply to the full reconstructed assertion.
There is no theoretical limitation since it is a straightforward
property of logic that
P => P' (P' is weaker than P) if and only if there exists
NP such that P' = P v NP
Q' => Q (Q' is stronger than Q) if and only if there exists
NQ such that Q' = Q ^ NQ
An absent ``require or'' clause means NP = false (no change to the
original precondition P); an absent ``ensure and'' clause means
NQ = true (no change to the original postcondition Q). This immediately
solves problem 2 above: in the common case in which the precondition or
postcondition or both do not change, you may just omit the ``require or''
or ``ensure and'' clause(s) altogether.
Discussion
----------
Some people have questioned the need for the ``or'' and ``and''
qualifiers. Since the rule is strict, and no other forms are possible,
why not say just ``require'' and ``ensure'' with the convention that
they mean or-ing/and-ing with the original when they apply to a
redefined version of a routine?
On closer look, this appears inappropriate. The danger is for
someone who looks at the text of a routine r out of context to believe
that the ``require'' clause expresses the full precondition, and similarly
for the other clause. By forcing ``require or'' and ``ensure and'',
you avoid such confusion.
Tool impact
-----------
An important tool in the Eiffel environment is the FLAT class
flattener, which reconstructs inheritance-free versions of a class
by expanding all the ancestors. In combination with the SHORT
interface documenter, this is a key documentation tool.
Clearly, when FLAT is applied to a redefined routine with
a ``require or'' or ``ensure and'' clause, it will reconstruct
the full pre/post condition by or-ing or and-ing with the original,
inherited version of the assertion.
A note on conversion of existing software
-----------------------------------------
To ease conversion of existing Eiffel classes, form [1] will
give rise to a non-fatal compile-time warning. Its presence
in a class text is indeed not catastrophic; simply, it precludes
enforcement of the weakening/strengthening principle.
-- Bertrand Meyer
bertrand@eiffel.com