Path: utzoo!attcan!uunet!know!zaphod.mps.ohio-state.edu!swrinde!ucsd!hub.ucsb.edu!eiffel!bertrand
From: bertrand@eiffel.UUCP (Bertrand Meyer)
Newsgroups: comp.object
Subject: Re: Void references
Summary: Some errors will remain
Message-ID: <451@eiffel.UUCP>
Date: 11 Nov 90 20:22:01 GMT
References: <447@eiffel.UUCP> <77500064@m.cs.uiuc.edu>
Organization: Interactive Software Engineering, Santa Barbara CA
Lines: 74


There is something strange in this discussion. In the messages
by Ralph Johnson and Craig Chambers one gets the impression
(please correct me if this is a wrong impression) that
it is possible to guarantee statically that no error will
ever occur at run-time. I don't see this as a fulfillable
goal theoretically or practically, short of taking either
or both of the following two measures:

1. Full-fledged program proving.
2. Unacceptable restrictions on the expressive power
   of the language (e.g. no references).

The aims of typing are more modest: guaranteeing statically
that a certain class of run-time errors will never occur.
Of course we should make that class as broad as possible.

Object-oriented technology is a particularly illuminating
context for discussing these issues because in a pure object-oriented
language such as Eiffel or Smalltalk, once you remove the supporting
machinery, the analysis/design/programming language has essentially
ONE operation: feature call, of the form

	x.f

Let us assume for a moment that f has no precondition (i.e. is always
applicable to an instance of the class in which f was declared).
Then the only problem of software reliability becomes:

/A/
	Can we statically guarantee that for every possible execution
	of x.f at run time, x will be attached to an object capable
	of handling feature f?

Because answering this question positively would require either
or both of 1. and 2. above and hence seems impossible, the most
useful practical solution seems to be to settle for the question

/B/
	Can we statically guarantee that for every possible execution
	of x.f at run time, if x is attached to an object, that object
	will be capable of handling feature f?

The answer in Eiffel to question /B/ is  ``yes in principle; with
Interactive's current compiler, yes in almost every case that counts'',
and we are working to transform this into a ``yes'' without qualification.

[Anyone familiar with axiomatic semantics will recognize in
the difference between /A/ and /B/ something similar to the difference
between total and partial correctness.]

The idea behind /B/ is to cover statically as many as possible of
the potential erroneous cases through type checking,
and to relegate every other case to a single type of error,
feature application to a void reference.

In practice, there remains another erroneous case, the one in
which f does have an object to work on, but the object does not satisfy
the precondition of f (e.g. f is extraction of the real square root
and x is an object representing a real number). Then /B/ becomes:

/B'/
	Can we statically guarantee that for every possible execution
	of x.f at run time, if x is attached to an object that satisfies
	the precondition of f, that object will be capable of handling f?

(Some practical cases that are handled differently at the implementation
level, such as arithmetic overflow or operating system signals, which
theoretically fall in this framework too.)

The situation with respect to precondition violations is the same as
for vacuity tests (checking whether x may be void): everyone would like
to check statically, but that is impossible in the general case
within the current state of program proving technology.

Of course, if we choose /B/ it is still essential to try to check
statically, as extensively as possible, that x will always be
non-void. In many cases this is possible or even trivial, as in

	x.Create;
	x.f ...

Similarly, if we consider /B'/ instead (which is necessary in practice)
we will try to ascertain statically, in as many cases as possible,
that all feature calls guarantee the corresponding precondition.
However:

	+ When it comes to static checking of both non-vacuity properties
	  and preconditions, we have to accept that the techniques that
	  work are NOT those commonly used for static type checking,
	  and that, short of solving 1. and 2. above, there is no universal
	  solution, only individual, specific and partial techniques.

	+ Whenever we have less than perfect faith in the exhaustiveness
	  of the static verification we may have performed, we need to rely
	  on dynamic checking: for every execution of x.f that has not been
	  proved correct, check at run-time that x is non-void and the
	  associated object satisfies the precondition of f.

In dynamic checking does detect anomaly, the only acceptable
solution is to raise an exception, which is why it is so essential
for any attempt at reliable object-oriented software to have a clean
exception handling facility, tied in to the assertion mechanism.

-- Bertrand Meyer
bertrand@eiffel.com