should postconditions be evaluated even if Exception is thrown?

[Michel Fortin]

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?

-- 
Michel Fortin
michel.fortin at michelf.com
http://michelf.com/