From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: ** X-Spam-Status: No, score=2.7 required=5.0 tests=BAYES_00,INVALID_DATE, PDS_OTHER_BAD_TLD,REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4 Path: utzoo!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!tut.cis.ohio-state.edu!python.cis.ohio-state.edu!holly From: holly@python.cis.ohio-state.edu (Joe Hollingsworth) Newsgroups: comp.lang.ada Subject: Re: Pre-condition vs. Post-condition Keywords: pre-condition, post-condition, exception Message-ID: <97779@tut.cis.ohio-state.edu> Date: 18 Mar 91 15:04:47 GMT References: <344@platypus.uofs.edu> <2865@sparko.gwu.edu> Sender: news@tut.cis.ohio-state.edu Reply-To: Joe Hollingsworth Organization: The Ohio State University Dept of Computer & Information Science List-Id: In article <2865@sparko.gwu.edu> mfeldman@seas.gwu.edu () writes: >>Say we have a function CAPITAL which, given a country's name, returns its >>capital city. If the given country does not exist, an exception COUNTRY_ERROR >>is raised. Should the given country's presence be listed as a pre-condition >>for this function, or should its absense (it doesn't exist) and the raising >>of COUNTRY_ERROR be listed as a post-condition? >> >>I brought this question up in class today and the outcome was a split decision. >>I think exception raising and/or handling is as valid an outcome of a function >>or procedure as any other outcome, so I'm tempted to cover the issue in the >>post-condition comment. My opponents believe that a function's pre-conditions >>should be the conditions under which it would complete "normally", that is, >>without any exceptions being raised. > >Hmmm. Interesting question. I have always taught - and thought of - pre- >conditions as a set of "contract terms" which, if they are met, would >obligate the function writer to write code that delivers the right results. >>From a verification point of view, I think you are correct that raising >an exception is a _valid_ outcome of the function, and so the function has >to be tested with cases of "bad" input to check that the exception indeed >is raised under those conditions. If the pre- and post-conditions are used >to drive tests (or formal verification), I agree that _explicit_ exception- >raising by the function is a post-condition matter: it needs to be tested. ....stuff deleted..... >Mike Feldman I'm glad you raised the point of formal verification. I'd like to point out how the use of exception handling complicates verification (be it formal or informal). Examine the following possible implementation for Pop (popping a stack). procedure pop(s: stack) -- this pop doesn't return the top of the stack, just discards it. begin if(not empty(s)) then -- pop the stack else raise underflow end pop; The point here is that there are 2 distinct paths through the procedure which will have to be verified with respect to the pre and post conditions (pre and post conditions not given). The two paths are easy to spot. Now look at another implementation of Pop based on Booch's stack package: procedure pop(s: stack) -- this pop doesn't return the top of the stack, just discards it. begin stack.top := stack.top - 1; exception when Constraint_Error => raise underflow end pop; Here there are also two paths through the procedure, but it's not so obvious to the reader (verifier) how the path through the exception handler gets taken. The verifier has to realize that the variable stack.top has been defined as Natural and that a Constraint_Error will be raised by the run time system when trying to set it to -1. Since the control flow in this example is not explicit, let's call it implicit. I believe that verifying (formally or informally) code written using implicit control flow is harder than code using explicit control flow. If this point is valid, one might then believe that code written using implicit control flow stands a better chance of NOT being verified correctly, especially if it is informally verified. What's more I also believe that using exceptions leads one toward this kind of programming (i.e. depending on implicit control flow). I'm a follower of many of the rules found in Kernighan & Plauger's "The Elements of Programming Style", two of those rules reads as follows: "Write clearly - don't be too clever." "Say what you mean, simply and directly." I believe that exception handling leads one to writing programs that are not as clear as they could be (see the second example above which doesn't say what it means simply and directly). With respect to verification, if the verifier is mechanical, then it probably doesn't matter if the code uses implicit or explicit control, the verifier will be able to handle it. But, when was the last time any of us used a mechanical verifier on our Ada programs? Chances are the verifier is the person writing the code, and that person is doing it informally. All the more reason to "Write clearly..." and "Say what you mean, simply and directly." The above arguments lead me to believe that exception handling should be used only sparingly (if at all)! (Mike, you wanted to get a debate going on this? The above opinions should help!) Joe Joe Hollingsworth Computer and Information Science @ OSU holly@cis.ohio-state.edu