should postconditions be evaluated even if Exception is thrown?
Andrei Alexandrescu
SeeWebsiteForEmail at erdani.org
Thu Dec 3 14:16:11 PST 2009
Walter Bright wrote:
> Brad Roberts wrote:
>> Walter Bright wrote:
>>> Andrei Alexandrescu wrote:
>>>> An exception (not an Error) is an expected and documented outcome of a
>>>> function. After having listened to those endless Boeing stories,
>>>> please listen to this one :o). Contract Programming covers the
>>>> correctness of a program, and exceptions are correct behavior. By your
>>>> very Boeing stories that I stoically endured, it seems like the
>>>> logical conclusion is that postconditions must be evaluated upon
>>>> exceptional return.
>>> Consider a constructor. It's postcondition is the class invariant is
>>> satisfied. If it throws, the object is not successfully constructed and
>>> the invariant does not hold.
>>
>> If the constructor fails, the object never existed. Nothing to
>> validate is valid.
>
> Right. And I can't see how you can validate the output of a function
> that failed. Let's say your function sorts an array, and the post
> condition is the array is sorted. So, what would the postcondition be if
> it failed?
>
> out (result)
> {
> assert(failed || isSorted(result));
> }
>
> ? What's the point?
I found one more example.
A function that transfers money from one account to another must provide
a postcondition even in the case of failure: no matter what, upon exit,
the sum of the monies in the accounts is preserved. The transfer itself
may fail for any number of complex reasons (overdraft, limit of
transfers per month reached, account has limited access etc.) but the
transfer function must in all cases preserve the total sum of funds in
the two involved accounts.
Andrei
More information about the Digitalmars-d
mailing list