should postconditions be evaluated even if Exception is thrown?

[Michel Fortin]

On 2009-12-03 19:31:37 -0500, Andrei Alexandrescu 
<SeeWebsiteForEmail at erdani.org> said:

> 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.

That'll only work if the lock is acquired outside of the function call. 
If the lock is acquired inside the function, pre- and post-conditions 
cannot be under the lock, and thus cannot check that.

I think this just show that you probably ought to have two functions: 
one acquiring the lock which calls the other one to do the actual 
processing, the later one can have the pre-/post-conditions. But you 
can't put a contract on the one acquiring the lock since the contract 
would be outside it.

Well, you could avoid it if labeling the function with @synchronized 
was sufficient, but for the case above you probably want two locks, or 
some sort of database transaction, which won't work with @synchronized.

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