Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!sun-barr!olivea!samsung!sdd.hp.com!uakari.primate.wisc.edu!aplcen!boingo.med.jhu.edu!haven!cs.wvu.wvnet.edu!eichmann
From: eichmann@cs.wvu.wvnet.edu (David Eichmann)
Newsgroups: comp.software-eng
Subject: Re: Reuse, Tolerance, and Tradeoffs (was Re: Tolerance)
Message-ID: <1256@h.cs.wvu.wvnet.edu>
Date: 8 Feb 91 20:53:04 GMT
References: <9102081637.AA07189@elephant.cis.ohio-state.edu>
Organization: WVU Statistics and Computer Science
Lines: 46

weide@CIS.OHIO-STATE.EDU (Bruce Weide) writes:
...
>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.
...

   This is actually a good argument for a form of "second-order"
compiler optimization.  We have a pre-condition asserted both in the
client code and the server code - when only one is needed.  I *do*
take the stance from pure paranoia that one or the other must
verify the pre-condition.

   However, I'm also sorry to say that I can see two immediate
dilemmas with such a s-o optimization:

   1) optimizing the is_empty away from the loop predicate obviously
screws up the implicit semantics of the original client program
text, but maintains the original intermodule dependencies.

   2) optimizing the is_empty away from the body of the client
maintains the implicit semantics of the client program, but introduces
a new form of intermodule dependency between the client and the
server - and forces deferral of the optimization of the server body
until after the compilation of the client.

- Dave
======
David Eichmann
Dept. of Statistics and Computer Science
West Virginia University                  Phone: (304) 293-3607
Morgantown, WV  26506                     Email: eichmann@a.cs.wvu.wvnet.edu