Output contract's arguements

[H. S. Teoh]

On Thu, Sep 19, 2013 at 02:07:09PM +0200, Joseph Rushton Wakeling wrote:
> On 19/09/13 12:44, monarch_dodra wrote:
> >If the function has already exited, then why is the state of he
> >arguments modified? I though pass by value meant that the function
> >operated on its own copy?
> 
> I don't see what else makes sense.  v is a local mutable value that
> only has sense inside the function, and the only way it makes sense
> for the out contract to interact with it is to check on its final
> state to make sure it hasn't taken on an insane value.
> 
> It's redundant to check its initial state because you can already do
> that with the in contract.

Oh? But what about:

	real sqrt(real x)
	in { assert(x >= 0.0); }
	out(result) {
		assert(abs(result*result - x) < EPSILON);
	}
	body {
		... // implementation here
	}

The out contract provides useful information to the user of the API as
to what characteristics to expect from the return value of the function.
But if x has been modified by the function body, then the out contract
is invalid and doesn't actually say anything useful, because it'd be
exposing implementation details to the API. Contracts are supposed to be
guarantees made to users of the API, not some kind of post-function
final state sanity checker (for that, one should insert assert's before
the return statement inside the function body).

At the very least, it would be nice to have access to x.old, as Eiffel
allegedly allows, if we insist on letting x refer to the copy of the
input value modified by the function body.


T

-- 
I am Ohm of Borg. Resistance is voltage over current.