On Thursday, 19 September 2013 at 13:02:15 UTC, Peter Alexander wrote:
> On Thursday, 19 September 2013 at 12:45:01 UTC, Joseph Rushton Wakeling wrote:
>> On 19/09/13 14:19, Peter Alexander wrote:
>>> You mean a separate copy from v?
>>>
>>> But surely then the copy would *always* be the same in the in-contract as it is
>>> in the out-contract? What's the point?
>>
>> It makes sense to be able to access v.old (or v.onEntry or whatever you want to call it) in the out contract, as then you could do some checks on the final value of v that are dependent on its entry value.
>
> Yes that makes sense, but I have no idea what the difference between the input and output contracts are in the original post. What errors will the output v != 0 check catch that the input v != 0 test not catch if they both use the input value of v?

That was a reduced example to show that v was modified. It prevented running the actual output contract which was:

size_t msb(T)(T v)
in
{
  assert(v != 0);
}
out(ret)
{
  assert(2^^ret <= v);
  assert(v < 2^^(ret + 1));
}
body
{
  size_t ret = 0;
  while(v >>= 1) ++ret;
  return ret;
}
//----

I want to calculate the msb, and in the out contract, I want to validate it is correct, by comparing it with what the input was.

In this case, this doesn't really work, since the input was "consumed".

On Thursday, 19 September 2013 at 13:55:54 UTC, monarch_dodra wrote:
> I want to calculate the msb, and in the out contract, I want to validate it is correct, by comparing it with what the input was.
>
> In this case, this doesn't really work, since the input was "consumed".

Ok, so you need this v.old that I believe other languages have. I don't think re-using v to mean the previous value of it would be a good idea. It's useful sometimes to check the final value of v on function exit too.

On 09/19/13 15:03, PauloPinto wrote:
> On Thursday, 19 September 2013 at 12:04:34 UTC, Artur Skawina wrote:
>> On 09/19/13 13:11, Peter Alexander wrote:
>>> On Thursday, 19 September 2013 at 11:07:07 UTC, Artur Skawina wrote:
>>>> On 09/19/13 12:58, Peter Alexander wrote:
>>>>> On Thursday, 19 September 2013 at 10:44:32 UTC, monarch_dodra wrote:
>>>>>> On Thursday, 19 September 2013 at 10:38:37 UTC, 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_.
>>>>>>
>>>>>> Exactly.
>>>>>>
>>>>>> 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?
>>>>>
>>>>> What exactly would you like this to do? v only exists inside the body of the function. There is no v after the function exits. If you check v in the output contract then you are checking the final value of v.
>>>>
>>>> That "final value of v" is not part of any contract, it's just a private local.
>>>
>>> I repeat my question then: what would you want this to do? As you say, v is a local copy, it cannot be part of a contract -- it cannot affect anything the client code sees.
>>
>> A contract only describes the /external/ interface (inputs, outputs
>> and visible state).
>> It makes no sense for it to depend on any local private variable of a
>> method; 'assert's in the function body can be used to verify the
>> implementation.
>> Leaking the internal state into the contracts has consequences, such as
>> making it much harder to use the same executable/library/archive for both
>> debug and contract-less builds (well, w/o duplicating all the code,
>> instead of reusing the bodies). Being able to easily check the contracts
>> at the exe<>dll boundary is important; if this requires using a different
>> library binary or causes massive bloat then this feature simply won't be
>> used much...
> 
> 
> Sorry but this is not like that.
> 
> Contracts also make use of invariants for the internal state of the object.
> 
> This is exactly what out conditions are suppose to validate.
> 
> - The internal invariants are still valid on function's exit
> - The returned value and parameters passed by reference have the expected values
> 
> At least if D is supposed to follow what Design by Contract means in languages that already provide it, specially Eiffel which is the language that gave birth to these ideas.

While I can see some value in verifying /internal/ state (and not just "visible" like i said above), it should be *persistent* state, ie not just something completely local to a method, that ceases to exist on exit. Asserts are there for checking local assumptions.

The practical aspect is -- iff you don't leak implementation details
then contracts in a dynamically loaded library can be handled like this:
compile the body of a function and its in/out/invariants as separate
functions, plus emit an extra one which calls the contract code in
addition to the original function. Now you can call, say, f() to execute
the overhead-less body, or call f_with_contracts() to run the extra checks
too. The cost of enabling contracts is small; just a slightly larger
binary, no runtime penalty, unless requested. And, as dynamic linking
already implies a level of indirection, the choice of running with or
without checking the contracts can even be done at *runtime*.
This is probably *the* most important use-case of contracts in a language
like D; if this can't be handled effciently, then D could just drop all
support for contracts.

Note that in the above scenario the compiler would need a three-way switch
"contracts = (None|Externally_visible|All). The 'All' case would cause all
emitted code to call the contracts - you'd use it while working on and
testing eg a library. Then, when you release it, you build it with
'contracts=Externally_visible', which will emit the contract funcs, but
will never actually /call/ them. This means that some /internal/ contracts
are not run, but that's ok, as in return you receive *zero* perf overhead.
You can now ship the dll as-is, and /the user/ gets to choose if he wants
to enable contract-checking. No need to worry about linking with right
version of the library; the support is always there. And the cost is
just a slightly larger file, that goes away if you recompile the lib with
'contracts=None' (or use a tool to strip the extra code).

Keeping the mistake, that exposing the local args was, not only makes no sense, but would prevent implementing saner contract support.

artur

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.

H. S. Teoh:

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

OK. But if x is a reference to a data structure, the old (prestate) needs to be just a shallow copy.

Bye,
bearophile

On Thu, Sep 19, 2013 at 04:44:12PM +0200, bearophile wrote:
> H. S. Teoh:
> 
> >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.
> 
> OK. But if x is a reference to a data structure, the old (prestate)
> needs to be just a shallow copy.
[...]

Hmm. So it seems there are two use cases here:

1) An argument is passed by value: in this case, the implementation details shouldn't be exposed, so only x.old should be referred to in the out contract.

2) An argument is mutable and passed by reference: in this case, the point of the function is presumably some side-effect on the argument, so the out contract generally should refer to the final state of the argument (so it serves as documentation on what the function does to the mutable argument). It may still be useful to refer to x.old in this case, but it would incur performance overhead (and possibly implementational difficulties since D currently doesn't have automatic deep-copying). So a shallow copy would be an acceptable compromise.


T

-- 
I've been around long enough to have seen an endless parade of magic new techniques du jour, most of which purport to remove the necessity of thought about your programming problem.  In the end they wind up contributing one or two pieces to the collective wisdom, and fade away in the rearview mirror. -- Walter Bright

On 19/09/13 16:39, H. S. Teoh wrote:
> 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.

I absolutely agree that access to x.old is needed, but I don't see the value or purpose in excluding the final value of x from the out checks -- it's useful to be able to check those values, too.

Joseph Rushton Wakeling:

> I don't see the value or purpose in excluding the final value of x from the out checks -- it's useful to be able to check those values, too.

Do you mean for all arguments, or just for the "out" ones?

int foo(out int x) { ...

Bye,
bearophile

On Thursday, 19 September 2013 at 15:18:21 UTC, Joseph Rushton Wakeling wrote:
> On 19/09/13 16:39, H. S. Teoh wrote:
>> 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.
>
> I absolutely agree that access to x.old is needed, but I don't see the value or purpose in excluding the final value of x from the out checks -- it's useful to be able to check those values, too.

It is it worth requiring the contract to actually know the final value of x?
Don't think so.

On 19/09/13 17:25, bearophile wrote:
> Joseph Rushton Wakeling:
>
>> I don't see the value or purpose in excluding the final value of x from the
>> out checks -- it's useful to be able to check those values, too.
>
> Do you mean for all arguments, or just for the "out" ones?
>
> int foo(out int x) { ...

I don't see why it shouldn't be all ... ?