On Thursday, 19 September 2013 at 18:27:52 UTC, H. S. Teoh wrote:
In my understanding, an out-contract is some condition C that the function F promises to the caller will hold after it has finished executing. Since F's internal state is uninteresting to the caller, C is expressed in terms of what is visible to the caller -- that is, the original function parameters and its return value(s) (which may include the final state of the parameters if changes to those parameters are visible to the caller). An out-contract shouldn't depend on the state of local variables in F, since those are not visible to the caller and are therefore uninteresting. If you wish to check that F's internal state satisfies some condition X at the end of F, then it should be done as assert(X) before return, not as an out-contract.
OK, you could define an out-contract that way -- but what's wrong in principle with the contract also being able to promise, "My internal state was sane on exit"?
Nitpicking over what should and shouldn't be allowed to be in contracts seems like a good way to complicate implementing them for no obvious technical benefit. Is there really any technical cost to allowing the out-contract to address internal function variables, if the programmer wants it?
