September 19, 2013
Am 19.09.2013 16:39, schrieb Artur Skawina:
> 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
>
>
>

For me saner contract support means what Eiffel and Ada allow for.

--
Paulo
September 19, 2013
On Thursday, 19 September 2013 at 10:29:22 UTC, monarch_dodra wrote:
> On Thursday, 19 September 2013 at 08:29:43 UTC, Maxim Fomin wrote:
>>> In particular if/when we will have "contracts are managed/compiled by caller", then that behavior is the only behavior we will be able to do (AFAIK).
>>>
>>
>> I looks like your misunderstanding based on wrong assumption about implementation.
>
> Not really a wrong assumption. This *has*. This has been discussed before. Another plan is to allow contracts in interfaces, in which case, there is no associated body:
> http://d.puremagic.com/issues/show_bug.cgi?id=6549

Interfaces are irrelevant here. By the way, taking into account current implementation I think you will have to wait a lot of time to see the requested satisfied. And even if it will be, nothing stops parameter to be modified by function body even it is not known at CT.

>
>>> Or is there something that explicitly states it works that way? Should I file a bug report? ER?
>>
>> I don't consider that whether out refers to unmodified or modified parameter is important issue. Current policy should be just documented and left as it is (unless you provide significant reasons that current implementation is flawed).
>
> It's flawed because the behavior of the contract will depend on what the body of the function does to copies of data that should be scoped only to that body.

This is deliberately created problem - you modify passed by value parameter which has little sense and then you make so that out contract should depend on original value of parameter. Now you create a problem and complain about it.

By the way, it seems that you view in/out/body as separate functions, probably like invariant, which is wrong - just take a look into assembly as I asked before. If you want to modify parameter, just create local copy of it.

>
> An "out" contract should only verify that the value returned is correct "in regards" to the "input arguments".
>
> This means the implementation details of the function's body are leaking into the out block. That just isn't right.

This is pure theory. Nothing promises you that discussed minor implementation detail of out contracts would be implemented in a way you expect.

There are several problem arising from your demand:
1) How much sense is in (providing support for) modifying passed by value parameter?
2) If parameter is passed by reference and supposed to be modified, this would engage into a conflict that original value should be preserved in.
3) Implementing your proposal would require - either creating three separate functions for in/out/body or putting pressure on to function frame stack + available registers for saving original values. Even this does not solve ref problem.

And on the advantage part of the proposal there is no reasoning except suspicious practice of modifying passed by value parameters and your words "I'd like the out contract to operate on its own copies of the function's arguments."

Of course, you can issue enhancement request writing that you 1) do not want to wake a local copy of parameter and 2) do want to modify passed by value parameter and 3) do want to see in the out contract original value (thus requiring 4a) either to create three separate functions instead of one or 4b trashing stack/registers), but I expect it would be closed with boldly WONTFIX.

I really doubt someone would write pull for a 'problem' which is solvable by:

    size_t ret = 0;
+++ T vv = v;
--- while(v >>= 1) ++ret;
+++ while(vv >>= 1) ++ret;
    return ret;

September 19, 2013
On 09/19/13 18:21, Paulo Pinto wrote:
> 
> For me saner contract support means what Eiffel and Ada allow for.

What's missing in D? (other than this args issue, which is just a minor detail and can be easily worked around)

artur
September 19, 2013
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.

Andrei
September 19, 2013
On 9/19/13 4:18 AM, 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.

This can confuse people who'd expect the converse. Also, indirect changes would add to the confusion. Then what to do about stuff by ref? auto ref?

I think it's safe to stick with the current behavior.


Andrei

September 19, 2013
On 9/19/13 4:31 AM, PauloPinto wrote:
> 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.

That reminds me we have no reasonable equivalent for Eiffel's "old".

Andrei

September 19, 2013
On 9/19/13 7:31 AM, Peter Alexander wrote:
> 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.

Well I have bad news. Consider:

interface A
{
    void fun(int x) out { assert(x == 42); }
}

class B : A
{
    void fun(int x) { x = 42; }
}

void main()
{
    A a = new B;
    a.fun(0);
}

This fails at run time, meaning in this particular case x will have the value before the call.


Andrei
September 19, 2013
On Thursday, 19 September 2013 at 17:25:37 UTC, Andrei Alexandrescu wrote:
> Well I have bad news. Consider:
>
> interface A
> {
>     void fun(int x) out { assert(x == 42); }
> }
>
> class B : A
> {
>     void fun(int x) { x = 42; }
> }
>
> void main()
> {
>     A a = new B;
>     a.fun(0);
> }
>
> This fails at run time, meaning in this particular case x will have the value before the call.

Is this by design? That seems inconsistent to me, but maybe I'm missing something.

This passes btw:

struct S
{
    int y;
}

interface A
{
    void fun(S x) out { assert(x.y == 42); }
}

class B : A
{
    void fun(S x) { x.y = 42; }
}

void main()
{
    A a = new B;
    a.fun(S(0));
}

So, sometimes it uses the old value and sometimes it uses the new value?
September 19, 2013
On 9/19/13 10:53 AM, Peter Alexander wrote:
[snip]
> So, sometimes it uses the old value and sometimes it uses the new value?

Time to press a bug report!

Andrei
September 19, 2013
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