should postconditions be evaluated even if Exception is thrown?

[Andrei Alexandrescu]

Don wrote:
> Andrei Alexandrescu wrote:
>> 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?
>>
>> Very, very interesting example that actually makes my point very nicely.
>>
>> If the function doesn't throw, the postcondition is that the array is 
>> sorted.
>>
>> If the function does throw, the postcondition is that the array has 
>> not lost any element. So at least you know that information wasn't lost.
>>
>> I can't believe this is working so well in my argument :o).
> 
> I don't understand why you think that. I can't believe it adds any value 
> whatsoever.
> It's just like checked exceptions, but with a much, much higher burden.

Checked exceptions are a very different beast. With a checked exception 
you must repeat statically all of the possible exceptions emerging from 
the function. But that information is next to useless. All that code is 
interested in is the throws-or-not bit.

Postconditions are different. They are checks on the outcome of 
functions. The bane of exceptions-based languages is that once an 
exception is thrown, there's no real guarantee of the state of the 
system. This is because functions are too often written only having the 
success case in mind and neglecting to think and document how the world 
remains in case an exception is thrown.

In the particular case of array sorting, if you use swap() throughout 
against elements of the array, the postcondition is always respected. 
But if you temporarily alter the array (e.g. by moving some of its 
elements off to temporary storage), then the postcondition is weaker - 
you're not guaranteed to even have the data in place if your comparison 
operator throws.

I think this is information that a client of sort would be interested in.


Andrei