Re: Pre-condition vs. Post-condition

[jng@sli.com (Mike Gilbert)]

>>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?
>>
>> ...
>
>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.
> ...
>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?
>
>Mike Feldman

I agree with Mike Feldman's description of a function's pre-conditions as a
contract, which, if satisfied, will cause the function to produce the
documented post-conditions, and, if violated, will produce an _unpredictable_
result.

Given this point of view, if a function guarantees to raise a specific
exception under certain pre-defined conditions, then the raising of that
exception must be considered to be part of the contract.  Because of the
guarantee of an exception, this case is very different from a function's
unpredictable behavior if preconditions are violated.

Thus, to answer the original question, the non-existence of a country causing
COUNTRY_ERROR to be raised should be listed as a post-condition.

If COUNTRY_ERROR is a post-condition, then the programmer has several options
for how to handle the possible COUNTRY_ERROR exception in the calling context:

	a If the programmer can guarantee that only valid countries will be
	  passed to CAPITAL, then, by the terms of the post-condition, the 
	  function will never raise COUNTRY_ERROR, and the calling context
	  doesn't have to allow for it.

	b If the programmer can't absolutely guarantee that the country name
	  is valid, but he doesn't expect to pass an invalid one, then the
	  choice of whether the calling context should handle COUNTRY_ERROR
	  depends on how robust the programmer wishes to make the program.

	  (For example, the country name could be generated by another function
	  which has not been formally verified but it believed to generate
	  correct output.)

	c If the programmer has no idea whether the country name is valid, then
	  the calling context had better handle COUNTRY_ERROR.  (For example,
	  the country name could be read as input from a user.)

Contrast these options with an alternate specification of CAPITAL in which the
country name must be valid as a pre-conditon, and thus an invalid country name
violates the function's contract.  With this specification, the function
CAPITAL will be _unpredictable_ if passed an invalid country name.  That is,
CAPITAL _could_ raise COUNTRY_ERROR, it _could_ raise any other exception, it
_could_ always return "SHANGRI-LA", it _could_ go into a loop, etc. etc.

So, if COUNTRY_ERROR is not a possible post-condition, then options "b" and
"c" above are not possible, because the programmer can't count on COUNTRY_ERROR
being raised.

What this all comes down to is that the post-conditions are what a function's
user can _count on_ given input that satisfies the pre-conditions.  Thus, since
the original question stated that COUNTRY_ERROR _is raised_ for a non-existent
country, then that specific exception should be listed as a post-condition.

Alternatively, if the original question had said something like "we've
currently implemented CAPITAL to raise COUNTRY_ERROR if the input country
doesn't exist, but we don't want to promise that it will always do so," then
users of CAPITAL would _not_ be able to count on that behavior, and then the
appropriate specification would be a pre-condition that the country must exist.

BTW, this is a distinction with a great deal of practical importance.  Many
large integrated software systems (e.g., a complex database package modified to
support distributed data by using a commercial network package) develop errors
because the integrator counts on behavior that a software package _currently_
exhibits (esp. under unusual circumstances), but that the developer never
intended to _guarantee_.  Then, when the next release of the software package
comes out, with different behavior under those circumstances, the integrated
system fails.

Mike Gilbert
Software Leverage