Output contract's arguements

[Joseph Rushton Wakeling]

On 19/09/13 22:43, H. S. Teoh wrote:
> I'm not saying that the compiler should purposely check and reject such
> uses. I'm saying that such uses are wrong usages of out-contracts.  It's
> not the compiler's job to reject a badly-designed class API, for example
> (it wouldn't know how to determine if something was badly-designed, in
> the first place), but that doesn't mean poor API design is a good idea.
>
> What the OP was concerned about was how to write an out-contract that
> references the *original* values of the function arguments, which is
> definitely a legitimate case that should be supported. This legitimate
> use case should take precedence over the wrong usage of referencing
> local variables in an out-contract (if indeed it's not worth the trouble
> to make the compiler reject the latter case).

I completely got monarchdodra's concerns, but I'm just not convinced that the 
right way to go about that is to redefine the contract implementation so that x 
refers to its value on entry.

An x.old or x.in syntax (however you want to write it) would address that need. 
  Enforcing "x in the out-contract means x at function entry" isn't possible 
without breaking the opportunity to use the out-contract to verify final 
internal state.

> There is an obvious benefit of using out-contracts correctly: the
> function becomes self-documenting:
>
> 	real sqrt(real x)
> 	in { assert(x >= 0.0); }
> 	out(result) { assert(abs(result*result - x) < EPSILON); }
> 	body { ... }
>
> Just by reading the contracts of sqrt, you know that (1) it expects its
> argument to be non-negative, and (2) its return value is the square root
> of x (i.e., the return value multiplied by itself is equal to x up to
> the specified precision).

Understood, but do you lose that much by insisting that the out contract uses 
x.in or (Eiffel-style) x.old to refer to the original value?

> But if 'x' in the out-contract refers to a possibly modified value of x
> rather than the original argument, then the out-contract is basically
> meaningless to the caller of this function, since, not knowing how sqrt
> is implemented, the final value of x could be anything, and any
> condition satisfied by x is of no relevance outside of sqrt itself.  And
> since it has no relevance outside of sqrt, why bother with out-contracts
> at all? Just put the assert inside the function body, where it belongs.
>
> The only case where the modified value of an argument is relevant is
> when the argument is passed by reference, and the caller can observe the
> effects of the function on it. For example:
>
> 	void sqrtInPlace(ref real x)
> 	in { assert(x >= 0.0); }
> 	out {
> 		// Note: .out and .in is just hypothetical syntax.
> 		assert(abs(x.out * x.out - x.in) < EPSILON);
> 	}
> 	body { ... }

I think this is a good reason for assuming that the out contract by default 
refers to final values, _unless_ you explicitly ask for x.in.

Why?  Because if you have an input passed by reference, and you mutate it, then 
the "expected" value of x when you call the out contract is definitely going to 
be its mutated value.  Same for an input passed by pointer, where the value it 
points to is changed.

So, if you accept that in _some cases_ the "expected" or natural behaviour is 
that x will refer to a mutated value, it's better for that expectation to be 
consistent across all types than to have to make special rules.

> The out-contract is very useful, because it tells the user exactly how
> the function will modify its argument, and what relation the final value
> has to the original value. Currently, however, we don't have .out
> syntax, so the above contract is inexpressible. Worse yet, in the current
> implementation, we may write:
>
> 	void sqrtInPlace(ref real x)
> 	in { assert(x >= 0.0); }
> 	out {
> 		// Does this x refer to the initial value of x, or the
> 		// final value?
> 		assert(x >= 0.0);
>
> 		// It sure looks like the initial value to me. Which
> 		// makes it totally pointless. But it actually refers to
> 		// the final value, which is non-obvious, and also of
> 		// limited benefit since we can't express a more
> 		// definite guarantee about its final value w.r.t. its
> 		// original value (i.e., that the final value squared
> 		// equals the original value up to a given precision).
> 	}
> 	body { ... }

I get the visual convenience of it, but the ambiguities around reference types, 
pointers, etc. suggest to me that it just can't be that simple.

>> Is there really any technical cost to allowing the out-contract to
>> address internal function variables, if the programmer wants it?
>
> There is no cost -- it currently already lets you do that. :)

... but you can't have "x in the out-contract means x on function entry" without 
breaking that possibility.

> But it's also useless, because then there is no benefit to using an
> out-contract as opposed to a plain old assert before the return
> statement. In terms of the final executable code, there is basically no
> advantage that an out-contract offers above an in-body assert statement.
> The added value of an out-contract is the documented (and
> runtime-checked) guarantee it provides to the users of the API.
> Referencing implementation details that the users of the API don't care
> about, such as local variables in the out-contract, invalidates this
> benefit, which makes it useless.

I get the conceptual and self-documenting elegance of it, I just think that it's 
a false elegance when you consider the special cases you'd have to work round.

     void foo(int *x)
       in { assert *x >= 0.0; }
      out { assert *x >= 0.0; }
     body { ... }

What's the "instinctive" understanding of what this means, in this case?  What's 
the sensible default behaviour?