Jump to page: 1 26  
Page
Thread overview
Output contract's arguements
Sep 18, 2013
monarch_dodra
Sep 18, 2013
w0rp
Sep 18, 2013
bearophile
Sep 19, 2013
Maxim Fomin
Sep 19, 2013
monarch_dodra
Sep 19, 2013
Maxim Fomin
Sep 19, 2013
monarch_dodra
Sep 19, 2013
monarch_dodra
Sep 19, 2013
Peter Alexander
Sep 19, 2013
Artur Skawina
Sep 19, 2013
Peter Alexander
Sep 19, 2013
monarch_dodra
Sep 19, 2013
PauloPinto
Sep 19, 2013
Peter Alexander
Sep 19, 2013
Peter Alexander
Sep 19, 2013
monarch_dodra
Sep 19, 2013
Peter Alexander
Sep 19, 2013
Peter Alexander
Sep 19, 2013
Artur Skawina
Sep 19, 2013
PauloPinto
Sep 19, 2013
Artur Skawina
Sep 19, 2013
Paulo Pinto
Sep 19, 2013
Artur Skawina
Sep 19, 2013
PauloPinto
Sep 19, 2013
H. S. Teoh
Sep 19, 2013
bearophile
Sep 19, 2013
H. S. Teoh
Sep 19, 2013
bearophile
Sep 19, 2013
Dicebot
Sep 19, 2013
H. S. Teoh
Sep 19, 2013
H. S. Teoh
Sep 20, 2013
H. S. Teoh
Sep 20, 2013
monarch_dodra
Sep 20, 2013
monarch_dodra
Sep 20, 2013
Dicebot
September 18, 2013
This came up in learn:
Say you have this code:

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

Question, can this output contract fail?

Apparently, it does fail, since it is passed the variable v, *after* the body of the function is done with it.

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

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

Or is there something that explicitly states it works that way? Should I file a bug report? ER?
September 18, 2013
There are probably implementation reasons for it working this way. I think it's perfectly acceptable for the majority of cases, and for the edge cases where you want something like this, you can of course always do this.

void foo(int y)
out(val) {
   ...
} body {
   int val;

   ...

   assert(y != 0);

   return val;
}

Of course, you'd need to return only at the end of the function for that, but there are ways around that, like inner functions, or perhaps goto end. (Although I don't advocate use of goto.)
September 18, 2013
monarch_dodra:

> 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".
>
> 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).
>
> Or is there something that explicitly states it works that way? Should I file a bug report? ER?

This is an example of "leaky abstraction", caused by the D implementation of contracts.
What is the behavior of Ada and C# contracts on this?

Bye,
bearophile
September 19, 2013
On Wednesday, 18 September 2013 at 12:11:03 UTC, monarch_dodra wrote:
> This came up in learn:
> Say you have this code:
>
> //----
> size_t msb(T)(T v)
> in
> {
>   assert(v != 0);
> }
> out(ret)
> {
>   assert(v != 0); //Fails? Passes?
> }
> body
> {
>   size_t ret = 0;
>   while(v >>= 1) ++ret;
>   return ret;
> }
> //----
>
> Question, can this output contract fail?

It may or may not fail depending on language definition and right now spec lacks clarification.

>
> Apparently, it does fail, since it is passed the variable v, *after* the body of the function is done with it.
>

It currently fails due to the way in-body-out are implemented: all block statements are united into essentially one function. Body block (or some other entity) doesn't 'pass' variable, it is out block which refers to local modified value is an issue (cmpl   $0x0,-0x8(%rbp)). You could find it yourself by looking into assembly.

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

Probably if you think that parameters should be 'passed'. I don't think that implementation should behave this way. I also find no reason why out contract should refer to unmodified argument.

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

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

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

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

It does operate on its copy.

You modified the copy inside the function. The value at the call site is not modified.

By the way, the is to be expected in Eiffel, Ada and .NET contracts.

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

artur
« First   ‹ Prev
1 2 3 4 5 6