should postconditions be evaluated even if Exception is thrown?

[Walter Bright]

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.