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=0.7 required=5.0 tests=BAYES_00,INVALID_DATE,
	MSGID_SHORT,REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no
	version=3.4.4
Path: utzoo!news-server.csri.toronto.edu!torsqnt!hybrid!scifi!bywater!uunet!seas.gwu.edu!mfeldman
From: mfeldman@seas.gwu.edu (Michael Feldman)
Newsgroups: comp.lang.ada
Subject: Re: Pre-condition vs. Post-condition
Keywords: pre-condition, post-condition, exception
Message-ID: <2865@sparko.gwu.edu>
Date: 15 Mar 91 19:07:50 GMT
References: <344@platypus.uofs.edu>
Reply-To: mfeldman@seas.gwu.edu ()
Organization: The George Washington University, Washington D.C.
List-Id: <comp.lang.ada>

>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.

Failure of a caller to meet a pre-condition violates the contract between
function writer and function user, in a way that the behavior of the
function is _unpredictable_, for example the actual parameter is 
unitialized. If the "garbage" in the parameter _happens_ to constitute
an in-range value, the function delivers a "correct" answer, coincidentally.
Otherwise, an exception may be _unexpectedly_ raised (constraint_error, say).
Since the caller has violated the contract, he gets what he deserves (an
unexpected propagation of an exception). So the pre-conditions are really
saying "if you violate these, all bets are off on what this function does."

This argument makes sense to me from a theoretical standpoint. From a 
practical standpoint, in describing the interface to a function, how does
one distinguish between violations that result in a _predictable_ behavior
and those that do not? I can see why your students may have disagreed.
It's a confusing matter. I'm posting this to the net to provoke other
readers to join this thread if they are interested.

Mike Feldman