Output contract's arguements

[H. S. Teoh]

On Fri, Sep 20, 2013 at 04:01:56PM +0200, Joseph Rushton Wakeling wrote:
> 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.

True. I agree that redefining plain "x" to mean "initial value of x"
would be difficult to implement for ref arguments, and will also break
existing code to boot. Having access to x.old is the best solution where
possible (I'm thinking, for the sake of implementational simplicity,
that we can restrict x.old to only work for parameters passed by value,
since D doesn't have a generic way of cloning a reference argument).


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

No, but the current notation is ambiguous and misleading. I agree that
x.in and x.out (or some such notation) is better.


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

I would rather say that it's illegal to refer to plain 'x' in an
out-contract because it's ambiguous. It should always refer to either
x.in or x.out. (Of course, we can silently still support the current
syntax in order to preserve backward compatibility, but I'd really
prefer it to be deprecated.)


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

It's better to be explicit about which version of the argument you're
referring to. Make it mandatory to write x.in and x.out. Then the
compiler can catch the cases where you wrote x.in but there is no
obvious way to implement it for a ref argument. Better have a
compile-time error than a runtime bug where you think x refers to x.in
but it actually refers to x.out.


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

OK, so we should make x.in and x.out mandatory syntax, and deprecate
straight references to unqualified x. That way, the above ambiguous code
will be rejected, and you will be forced to write in unambiguously.


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

This issue is fixed if we make x.in and x.out mandatory.


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

I'd say this is a good argument for making x.in and x.out mandatory
syntax. Then it becomes clear and readable:

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

And for moving non-contract asserts (i.e. those that check
implementation sanity rather than make any guarantees of interest to the
caller) into the function body rather than putting them in the
out-contract.


T

-- 
Живёшь только однажды.