On 2009-12-03 19:31:37 -0500, Andrei Alexandrescu
<[email protected]> said:
Michel Fortin wrote:
On 2009-12-03 17:16:11 -0500, Andrei Alexandrescu
<[email protected]> 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
[email protected]
http://michelf.com/
