Path: utzoo!utgpu!news-server.csri.toronto.edu!bonnie.concordia.ca!uunet!tut.cis.ohio-state.edu!CIS.OHIO-STATE.EDU!weide
From: weide@CIS.OHIO-STATE.EDU (Bruce Weide)
Newsgroups: comp.software-eng
Subject: Re: Reuse, Tolerance, and Tradeoffs (was Re: Tolerance)
Message-ID: <9102081637.AA07189@elephant.cis.ohio-state.edu>
Date: 8 Feb 91 16:37:35 GMT
Sender: weide@tut.cis.ohio-state.edu
Lines: 96

Nancy,

Perhaps my one-sentence summary of the issue was not clear.  There are
two important points I'd like to make in order to clarify the position
that a most-reusable stack abstraction should NOT involve a test for
emptiness during the "pop" operation.

(1) We are working in a system in which components DO have formal
specifications and in which programs are verified.  Of course most
real-world software today is not carefully specified or verified, but
we're arguing that new-generation software SHOULD be.  I guess we
agree on that; or maybe not?

In any case, the formal specification of pop in our stack component
includes an explicit precondition that the stack is not empty.  This
means that the implementer is free to assume that the stack being
popped is not empty -- and therefore need not test for it -- and that
the client is obligated to be able to demonstrate this fact wherever
pop is called.  For instance, consider stack s as used in the
following program fragment (actually, quite a typical use):

	while not is_empty (s) do
		pop (s, x);
		...
	end while;

There is no problem verifying that pop's precondition is satisfied for
this use of pop.  Why, then, should another check for emptiness be
made inside the implementation of pop?  The client program has just
checked that.

(2) In no way did I mean to imply that client programs should not
check for errors, when it is appropriate.  I am quite fond of your
work on software safety and I appreciate your examples and the points
you make about it.  My point does not conflict in any way.  It is that
reusable software components should be designed to permit maximum
reuse, through judicious use of layering.  One obvious way to reuse
the stack component I proposed is to make it a building block for a
"safe" or "defensive" stack component in which pop does something
quite predictable if the stack is empty.  (The specification of this
version of pop includes the desired behavior for an empty stack in its
postcondition, and its precondition is simply "true.")

Now you have at least two choices: you can layer the non-defensive
stack component on top of the defensive one, or vice versa.  The
problem with putting the defensive design in the lower layer is that a
client (such as the one above) who can PROVE that pop will never get
an empty stack must pay for a redundant test for emptiness.  Now this
may not seem like a big problem here because stacks are simple and
it's presumably easy and fast to test this condition.  However, there
are other cases where that is not true, and substantial performance
penalties are incurred because of the insistence that EVERY reusable
module (even the lowest level ones) be completely defensive.


While I'm writing, there is something else you said that puzzles me:

 "Sure, you can write down all the assumptions made by the developers
 (e.g., an empty stack will never be popped) and the user can check
 for them -- easier for something like a stack where we have been
 exploring what those assumptions are in hundreds of papers for the
 past 20 years than in other software...  We are not even aware of
 many (if not most) assumptions we make in programming.  Formal
 specifications will help somewhat, but there are lots of cases of
 incomplete formal specifications for even simple things like stacks
 being written.  We have a paper coming out in the March issue of IEEE
 Trans. on Soft. Eng. that attempts to define the assumptions you need
 to specify, but it does not completely solve this problem."

Apaprently your point is that formal specification will be hard for
more complex abstractions than stacks.  Agreed.  Not impossible (we've
got dozens of examples to prove it), but harder than for stacks.
That's why we're working on it: it's an interesting research problem.
But if your conclusion is true, how do you propose to write software
that TESTS that these assumptions are satisfied if you can't even
write down what the assumptions are?  If you can write them down,
great, put them in the specification.  If not, seems like you're
doomed to have software that crashes sometimes.  I don't see how this
is an attack on the idea of formal specification, or on our arguments
about design-for-reuse.


In fact, if I might be allowed to speculate a bit about some of the
difficulties with real-time programs that constitute many of your
examples of problem software... I do have some experience in this
area.  It is precisely a concern with efficiency (even constant
factors) that leads many real-time systems folks to eschew well-tested
and possibly verified reusable software components in favor of
one-time, ad hoc components that are far more likely to contain errors
in design or implementation.  Reusable components MUST be efficient,
as well as correct, if we really expect them to be reused.  To deny
that things like unnecessary checks of preconditions have any
influence over how real-time software is actually written seems fairly
implausible to me.

	-Bruce