Output contract's arguements

[Joseph Rushton Wakeling]

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?