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.

On Thursday, 19 September 2013 at 11:11:58 UTC, Peter Alexander wrote:
> On Thursday, 19 September 2013 at 11:07:07 UTC, Artur Skawina
>> 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.

I'd like the out contract to operate on its own copies of the function's arguments.

These could either be passed by the implementation of the body, prior to starting proper, or by the caller, passing the same arguments to both the contract and the function. That'd be dependent on the implementation.

On Thursday, 19 September 2013 at 11:18:54 UTC, monarch_dodra wrote:
> On Thursday, 19 September 2013 at 11:11:58 UTC, Peter Alexander wrote:
>> On Thursday, 19 September 2013 at 11:07:07 UTC, Artur Skawina
>>> 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.
>
> I'd like the out contract to operate on its own copies of the function's arguments.
>
> These could either be passed by the implementation of the body, prior to starting proper, or by the caller, passing the same arguments to both the contract and the function. That'd be dependent on the implementation.

Using the Eiffel standard as reference, chapter 8.9, the daddy of design by contract

http://www.ecma-international.org/publications/standards/Ecma-367.htm

Given a parameter x, on a postcondition it refers to the local value on function's exit. To refer to the original value on entry it needs to be prefixed with the keyword old.

--
Paulo

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

artur

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.

On 19/09/13 14:04, Artur Skawina wrote:
> 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...

That seems to be a theoretical ideal that doesn't acknowledge the practical benefits of being able to check final values of local function variables on exit.

I'm not sure that it can really be described as leaking given how contracts are apparently implemented in a practical sense.

On Thursday, 19 September 2013 at 11:18:54 UTC, monarch_dodra wrote:
> On Thursday, 19 September 2013 at 11:11:58 UTC, Peter Alexander wrote:
>> On Thursday, 19 September 2013 at 11:07:07 UTC, Artur Skawina
>>> 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.
>
> I'd like the out contract to operate on its own copies of the function's arguments.
>
> These could either be passed by the implementation of the body, prior to starting proper, or by the caller, passing the same arguments to both the contract and the function. That'd be dependent on the implementation.

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?

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.

e.g. you might have a function where this kind of rule holds:

    assert((v && !v.old) || (!v && v.old));

i.e. if it's 0 on entry, it must be non-zero on exit, and vice versa.

But it doesn't make sense to me that v in the out contract would refer to the value of v on entry to the function.

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?

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


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.

--
Paulo