should postconditions be evaluated even if Exception is thrown?

[Walter Bright]

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?