Output contract's arguements

[H. S. Teoh]

On Thu, Sep 19, 2013 at 10:11:21AM -0700, Andrei Alexandrescu wrote:
> On 9/19/13 3:38 AM, Joseph Rushton Wakeling wrote:
> >On 18/09/13 14:11, monarch_dodra wrote:
> >>IMO, this is wrong. When calling a function with an out contract,
> >>the arguments should *also* be passed to the out contract directly.
> >>"out" should not be expected to run on the body's "sloppy seconds".
> >
> >I'm not sure I understand your objection here.  As I understood it
> >the whole point of an "out" contract was to check the state of
> >everything _after the function has exited_.
> 
> Agreed.
[...]

In that case, your definition of "contract" is different from mine.

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.

Mutable arguments passed by reference obviously makes sense to be
included in an out-contract, since you presumably want to provide some
guarantees to the user that after F runs, the (possibly-changed) state
of a mutable ref argument satisfies some condition C.

Arguments passed by value, though, is a special case: the changes F
makes to them are not visible to the caller, so they are essentially
local variables whose initial values are specified by the caller. Hence,
referring to their final value in an out-contract makes no sense. If I
pass an int x to F, then an out-contract that tells me that x will have
the value 17 after F finishes is completely irrelevant to me, because I
don't have access to the final value of x anyway, and I don't care.  F's
implementor may care, since it may be an indication of whether the
implementation of F is correct, but in that case, an assert(x==17) at
the end of the function body should be used, not an out-contract.

So having access to the original copies of parameters is necessary, so
you could write:

	real sqrt(real x)
	in { assert(x >= 0.0); }
	out { assert(abs(x.in * x.in) < EPSILON); }
	body {
		... // implementation here
		x /= 2; // suppose we modify x at some point
		... // more implementation

		// Suppose our sqrt algorithm for whatever reason ends
		// with x=1 and if that's not true, then the code is
		// broken. The caller doesn't and shouldn't care about
		// this, so this doesn't belong in an out-contract, it
		// belongs in an assert inside the function body.
		assert(x == 1.0);

		return result;
	}

We could use x.in and x.out to unambiguously refer to original/final
values of parameters. Using the keywords in/out also means that it can
never be confused with member variables or UFCS, so it's nice to have.


T

-- 
Arise, you prisoners of Windows
Arise, you slaves of Redmond, Wash,
The day and hour soon are coming
When all the IT folks say "Gosh!"
It isn't from a clever lawsuit
That Windowsland will finally fall,
But thousands writing open source code
Like mice who nibble through a wall.
-- The Linux-nationale by Greg Baker