should postconditions be evaluated even if Exception is thrown?

[Andrei Alexandrescu]

Michel Fortin wrote:
> On 2009-12-03 17:16:11 -0500, Andrei Alexandrescu 
> <SeeWebsiteForEmail at erdani.org> said:
> 
>> 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.
> 
> That's a good example.
> 
> But make this multithreaded and you have to hold the lock or transaction 
> across the function and its pre- and post-conditions. Where should we stop?
> 

I'd think the pre- and postconditions msut be under the lock anyhow.

Andrei