should postconditions be evaluated even if Exception is thrown?

[Don]

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.