www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - Output contract's arguements

reply "monarch_dodra" <monarchdodra gmail.com> writes:
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?
Sep 18 2013
next sibling parent "w0rp" <devw0rp gmail.com> writes:
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.)
Sep 18 2013
prev sibling next sibling parent "bearophile" <bearophileHUGS lycos.com> writes:
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.


Bye,
bearophile
Sep 18 2013
prev sibling next sibling parent reply "Maxim Fomin" <maxim maxim-fomin.ru> writes:
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).
Sep 19 2013
parent reply "monarch_dodra" <monarchdodra gmail.com> writes:
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.
Sep 19 2013
parent reply "Maxim Fomin" <maxim maxim-fomin.ru> writes:
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;
Sep 19 2013
parent "monarch_dodra" <monarchdodra gmail.com> writes:
On Thursday, 19 September 2013 at 17:09:49 UTC, Maxim Fomin wrote:

 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.


Yes, most probably. I'd much rather have the "in/out contracts 
should be conditionally included depending on caller compilation 
options, the lib's". EG: the reason druntime doesn't do array 
overlap checking, even when compiling in non-release.


 And even if it will be, nothing stops parameter to be modified 
 by function body even it is not known at CT.


I didn't suggest banning modifying function arguments?


 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.


Just to be clear, I'm not complaining. I wanted to have a clearer 
answer about what the behavior *should* be. To be fair, I 
expected the answer would be "It should probably work that way, 
but it'll never happen, sorry".


 By the way, it seems that you view in/out/body as separate 
 functions, probably like invariant, which is wrong


Why is it wrong? Is there a specification that says it *can't* be 
that way? It'd be (almost) the only way to be able to define 
contracts in interface files, with implementation inside other 
files.


 just take a look into assembly as I asked before.


My original question was "is the behavior according to spec". 
Looking at assembly defeats the question.


 If you want to modify parameter, just create local copy of it.


Yes.


 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.


Pure theory was the point of my question.


 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.


I'm perfectly fine if we close this as "won't fix", "for 
practical reasons, arguments passed by value *may* be modified by 
the implementation". As long as we document it right.


 Even this does not solve ref problem.


I'm not sure there is any problems with ref. Reference argument 
would reference the same variable regardless. I'm not asking for 
a time machine to give me the ref's old value.


 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 think I'm seeing a trend that, regardless of merit or technical 
correctness, changing the behavior excessively costly anyways.

:/
Sep 19 2013
prev sibling parent reply Joseph Rushton Wakeling <joseph.wakeling webdrake.net> writes:
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_.
Sep 19 2013
next sibling parent reply "monarch_dodra" <monarchdodra gmail.com> writes:
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?
Sep 19 2013
next sibling parent reply "Peter Alexander" <peter.alexander.au gmail.com> writes:
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.
Sep 19 2013
parent reply Artur Skawina <art.08.09 gmail.com> writes:
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
Sep 19 2013
parent reply "Peter Alexander" <peter.alexander.au gmail.com> writes:
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.
Sep 19 2013
next sibling parent reply "monarch_dodra" <monarchdodra gmail.com> writes:
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.
Sep 19 2013
next sibling parent reply "PauloPinto" <pjmlp progtools.org> writes:
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
Sep 19 2013
parent Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
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
Sep 19 2013
prev sibling next sibling parent reply "Peter Alexander" <peter.alexander.au gmail.com> writes:
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?
Sep 19 2013
parent reply Joseph Rushton Wakeling <joseph.wakeling webdrake.net> writes:
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.
Sep 19 2013
parent reply "Peter Alexander" <peter.alexander.au gmail.com> writes:
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?
Sep 19 2013
parent reply "monarch_dodra" <monarchdodra gmail.com> writes:
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".
Sep 19 2013
parent reply "Peter Alexander" <peter.alexander.au gmail.com> writes:
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.
Sep 19 2013
parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
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
Sep 19 2013
parent reply "Peter Alexander" <peter.alexander.au gmail.com> writes:
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?
Sep 19 2013
parent Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
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
Sep 19 2013
prev sibling parent Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
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
Sep 19 2013
prev sibling next sibling parent reply Artur Skawina <art.08.09 gmail.com> writes:
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
Sep 19 2013
parent reply "PauloPinto" <pjmlp progtools.org> writes:
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
Sep 19 2013
parent reply Artur Skawina <art.08.09 gmail.com> writes:
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
Sep 19 2013
parent reply Paulo Pinto <pjmlp progtools.org> writes:
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
Sep 19 2013
parent Artur Skawina <art.08.09 gmail.com> writes:
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
Sep 19 2013
prev sibling parent Joseph Rushton Wakeling <joseph.wakeling webdrake.net> writes:
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.
Sep 19 2013
prev sibling next sibling parent "PauloPinto" <pjmlp progtools.org> writes:
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
Sep 19 2013
prev sibling next sibling parent Joseph Rushton Wakeling <joseph.wakeling webdrake.net> writes:
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.
Sep 19 2013
prev sibling next sibling parent reply "H. S. Teoh" <hsteoh quickfur.ath.cx> writes:
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.
Sep 19 2013
parent reply "bearophile" <bearophileHUGS lycos.com> writes:
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
Sep 19 2013
parent "H. S. Teoh" <hsteoh quickfur.ath.cx> writes:
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
Sep 19 2013
prev sibling parent reply Joseph Rushton Wakeling <joseph.wakeling webdrake.net> writes:
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.
Sep 19 2013
next sibling parent reply "bearophile" <bearophileHUGS lycos.com> writes:
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
Sep 19 2013
parent Joseph Rushton Wakeling <joseph.wakeling webdrake.net> writes:
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 ... ?
Sep 19 2013
prev sibling parent "Dicebot" <public dicebot.lv> writes:
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.
Sep 19 2013
prev sibling parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
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
Sep 19 2013
parent reply "H. S. Teoh" <hsteoh quickfur.ath.cx> writes:
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
Sep 19 2013
parent reply "Joseph Rushton Wakeling" <joseph.wakeling webdrake.net> writes:
On Thursday, 19 September 2013 at 18:27:52 UTC, H. S. Teoh wrote:

 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.


OK, you could define an out-contract that way -- but what's wrong 
in principle with the contract also being able to promise, "My 
internal state was sane on exit"?

Nitpicking over what should and shouldn't be allowed to be in 
contracts seems like a good way to complicate implementing them 
for no obvious technical benefit.  Is there really any technical 
cost to allowing the out-contract to address internal function 
variables, if the programmer wants it?
Sep 19 2013
next sibling parent "H. S. Teoh" <hsteoh quickfur.ath.cx> writes:
On Thu, Sep 19, 2013 at 09:46:35PM +0200, Joseph Rushton Wakeling wrote:

 On Thursday, 19 September 2013 at 18:27:52 UTC, H. S. Teoh wrote:

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.


 
 OK, you could define an out-contract that way -- but what's wrong in
 principle with the contract also being able to promise, "My internal
 state was sane on exit"?


Use an assert. That's what asserts are meant for.

And if you have multiple return statements and don't want to duplicate
code, just write:

	scope(exit) assert(myStateIsSane);

at the top of the function.



 Nitpicking over what should and shouldn't be allowed to be in
 contracts seems like a good way to complicate implementing them for
 no obvious technical benefit.


I'm not saying that the compiler should purposely check and reject such
uses. I'm saying that such uses are wrong usages of out-contracts.  It's
not the compiler's job to reject a badly-designed class API, for example
(it wouldn't know how to determine if something was badly-designed, in
the first place), but that doesn't mean poor API design is a good idea.

What the OP was concerned about was how to write an out-contract that
references the *original* values of the function arguments, which is
definitely a legitimate case that should be supported. This legitimate
use case should take precedence over the wrong usage of referencing
local variables in an out-contract (if indeed it's not worth the trouble
to make the compiler reject the latter case).

There is an obvious benefit of using out-contracts correctly: the
function becomes self-documenting:

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

Just by reading the contracts of sqrt, you know that (1) it expects its
argument to be non-negative, and (2) its return value is the square root
of x (i.e., the return value multiplied by itself is equal to x up to
the specified precision).

But if 'x' in the out-contract refers to a possibly modified value of x
rather than the original argument, then the out-contract is basically
meaningless to the caller of this function, since, not knowing how sqrt
is implemented, the final value of x could be anything, and any
condition satisfied by x is of no relevance outside of sqrt itself.  And
since it has no relevance outside of sqrt, why bother with out-contracts
at all? Just put the assert inside the function body, where it belongs.

The only case where the modified value of an argument is relevant is
when the argument is passed by reference, and the caller can observe the
effects of the function on it. For example:

	void sqrtInPlace(ref real x)
	in { assert(x >= 0.0); }
	out {
		// Note: .out and .in is just hypothetical syntax.
		assert(abs(x.out * x.out - x.in) < EPSILON);
	}
	body { ... }

The out-contract is very useful, because it tells the user exactly how
the function will modify its argument, and what relation the final value
has to the original value. Currently, however, we don't have .out
syntax, so the above contract is inexpressible. Worse yet, in the current 
implementation, we may write:

	void sqrtInPlace(ref real x)
	in { assert(x >= 0.0); }
	out {
		// Does this x refer to the initial value of x, or the
		// final value?
		assert(x >= 0.0);

		// It sure looks like the initial value to me. Which
		// makes it totally pointless. But it actually refers to
		// the final value, which is non-obvious, and also of
		// limited benefit since we can't express a more
		// definite guarantee about its final value w.r.t. its
		// original value (i.e., that the final value squared
		// equals the original value up to a given precision).
	}
	body { ... }



 Is there really any technical cost to allowing the out-contract to
 address internal function variables, if the programmer wants it?


There is no cost -- it currently already lets you do that. :)

But it's also useless, because then there is no benefit to using an
out-contract as opposed to a plain old assert before the return
statement. In terms of the final executable code, there is basically no
advantage that an out-contract offers above an in-body assert statement.
The added value of an out-contract is the documented (and
runtime-checked) guarantee it provides to the users of the API.
Referencing implementation details that the users of the API don't care
about, such as local variables in the out-contract, invalidates this
benefit, which makes it useless.


T

-- 
Just because you can, doesn't mean you should.
Sep 19 2013
prev sibling next sibling parent Joseph Rushton Wakeling <joseph.wakeling webdrake.net> writes:
On 19/09/13 22:43, H. S. Teoh wrote:

 I'm not saying that the compiler should purposely check and reject such
 uses. I'm saying that such uses are wrong usages of out-contracts.  It's
 not the compiler's job to reject a badly-designed class API, for example
 (it wouldn't know how to determine if something was badly-designed, in
 the first place), but that doesn't mean poor API design is a good idea.

 What the OP was concerned about was how to write an out-contract that
 references the *original* values of the function arguments, which is
 definitely a legitimate case that should be supported. This legitimate
 use case should take precedence over the wrong usage of referencing
 local variables in an out-contract (if indeed it's not worth the trouble
 to make the compiler reject the latter case).


I completely got monarchdodra's concerns, but I'm just not convinced that the 
right way to go about that is to redefine the contract implementation so that x 
refers to its value on entry.

An x.old or x.in syntax (however you want to write it) would address that need. 
  Enforcing "x in the out-contract means x at function entry" isn't possible 
without breaking the opportunity to use the out-contract to verify final 
internal state.


 There is an obvious benefit of using out-contracts correctly: the
 function becomes self-documenting:

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

 Just by reading the contracts of sqrt, you know that (1) it expects its
 argument to be non-negative, and (2) its return value is the square root
 of x (i.e., the return value multiplied by itself is equal to x up to
 the specified precision).


Understood, but do you lose that much by insisting that the out contract uses 
x.in or (Eiffel-style) x.old to refer to the original value?


 But if 'x' in the out-contract refers to a possibly modified value of x
 rather than the original argument, then the out-contract is basically
 meaningless to the caller of this function, since, not knowing how sqrt
 is implemented, the final value of x could be anything, and any
 condition satisfied by x is of no relevance outside of sqrt itself.  And
 since it has no relevance outside of sqrt, why bother with out-contracts
 at all? Just put the assert inside the function body, where it belongs.

 The only case where the modified value of an argument is relevant is
 when the argument is passed by reference, and the caller can observe the
 effects of the function on it. For example:

 	void sqrtInPlace(ref real x)
 	in { assert(x >= 0.0); }
 	out {
 		// Note: .out and .in is just hypothetical syntax.
 		assert(abs(x.out * x.out - x.in) < EPSILON);
 	}
 	body { ... }


I think this is a good reason for assuming that the out contract by default 
refers to final values, _unless_ you explicitly ask for x.in.

Why?  Because if you have an input passed by reference, and you mutate it, then 
the "expected" value of x when you call the out contract is definitely going to 
be its mutated value.  Same for an input passed by pointer, where the value it 
points to is changed.

So, if you accept that in _some cases_ the "expected" or natural behaviour is 
that x will refer to a mutated value, it's better for that expectation to be 
consistent across all types than to have to make special rules.


 The out-contract is very useful, because it tells the user exactly how
 the function will modify its argument, and what relation the final value
 has to the original value. Currently, however, we don't have .out
 syntax, so the above contract is inexpressible. Worse yet, in the current
 implementation, we may write:

 	void sqrtInPlace(ref real x)
 	in { assert(x >= 0.0); }
 	out {
 		// Does this x refer to the initial value of x, or the
 		// final value?
 		assert(x >= 0.0);

 		// It sure looks like the initial value to me. Which
 		// makes it totally pointless. But it actually refers to
 		// the final value, which is non-obvious, and also of
 		// limited benefit since we can't express a more
 		// definite guarantee about its final value w.r.t. its
 		// original value (i.e., that the final value squared
 		// equals the original value up to a given precision).
 	}
 	body { ... }


I get the visual convenience of it, but the ambiguities around reference types, 
pointers, etc. suggest to me that it just can't be that simple.


 Is there really any technical cost to allowing the out-contract to
 address internal function variables, if the programmer wants it?


 There is no cost -- it currently already lets you do that. :)


... but you can't have "x in the out-contract means x on function entry"
without 
breaking that possibility.


 But it's also useless, because then there is no benefit to using an
 out-contract as opposed to a plain old assert before the return
 statement. In terms of the final executable code, there is basically no
 advantage that an out-contract offers above an in-body assert statement.
 The added value of an out-contract is the documented (and
 runtime-checked) guarantee it provides to the users of the API.
 Referencing implementation details that the users of the API don't care
 about, such as local variables in the out-contract, invalidates this
 benefit, which makes it useless.


I get the conceptual and self-documenting elegance of it, I just think that
it's 
a false elegance when you consider the special cases you'd have to work round.

     void foo(int *x)
       in { assert *x >= 0.0; }
      out { assert *x >= 0.0; }
     body { ... }

What's the "instinctive" understanding of what this means, in this case? 
What's 
the sensible default behaviour?
Sep 20 2013
prev sibling next sibling parent reply "H. S. Teoh" <hsteoh quickfur.ath.cx> writes:
On Fri, Sep 20, 2013 at 04:01:56PM +0200, Joseph Rushton Wakeling wrote:

 On 19/09/13 22:43, H. S. Teoh wrote:

I'm not saying that the compiler should purposely check and reject
such uses. I'm saying that such uses are wrong usages of
out-contracts.  It's not the compiler's job to reject a
badly-designed class API, for example (it wouldn't know how to
determine if something was badly-designed, in the first place), but
that doesn't mean poor API design is a good idea.

What the OP was concerned about was how to write an out-contract that
references the *original* values of the function arguments, which is
definitely a legitimate case that should be supported. This
legitimate use case should take precedence over the wrong usage of
referencing local variables in an out-contract (if indeed it's not
worth the trouble to make the compiler reject the latter case).


 
 I completely got monarchdodra's concerns, but I'm just not convinced
 that the right way to go about that is to redefine the contract
 implementation so that x refers to its value on entry.
 
 An x.old or x.in syntax (however you want to write it) would address
 that need.  Enforcing "x in the out-contract means x at function
 entry" isn't possible without breaking the opportunity to use the
 out-contract to verify final internal state.


True. I agree that redefining plain "x" to mean "initial value of x"
would be difficult to implement for ref arguments, and will also break
existing code to boot. Having access to x.old is the best solution where
possible (I'm thinking, for the sake of implementational simplicity,
that we can restrict x.old to only work for parameters passed by value,
since D doesn't have a generic way of cloning a reference argument).



There is an obvious benefit of using out-contracts correctly: the
function becomes self-documenting:

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

Just by reading the contracts of sqrt, you know that (1) it expects
its argument to be non-negative, and (2) its return value is the
square root of x (i.e., the return value multiplied by itself is
equal to x up to the specified precision).


 
 Understood, but do you lose that much by insisting that the out
 contract uses x.in or (Eiffel-style) x.old to refer to the original
 value?


No, but the current notation is ambiguous and misleading. I agree that
x.in and x.out (or some such notation) is better.


[...]

The only case where the modified value of an argument is relevant is
when the argument is passed by reference, and the caller can observe
the effects of the function on it. For example:

	void sqrtInPlace(ref real x)
	in { assert(x >= 0.0); }
	out {
		// Note: .out and .in is just hypothetical syntax.
		assert(abs(x.out * x.out - x.in) < EPSILON);
	}
	body { ... }


 
 I think this is a good reason for assuming that the out contract by
 default refers to final values, _unless_ you explicitly ask for x.in.


I would rather say that it's illegal to refer to plain 'x' in an
out-contract because it's ambiguous. It should always refer to either
x.in or x.out. (Of course, we can silently still support the current
syntax in order to preserve backward compatibility, but I'd really
prefer it to be deprecated.)



 Why?  Because if you have an input passed by reference, and you
 mutate it, then the "expected" value of x when you call the out
 contract is definitely going to be its mutated value.  Same for an
 input passed by pointer, where the value it points to is changed.
 
 So, if you accept that in _some cases_ the "expected" or natural
 behaviour is that x will refer to a mutated value, it's better for
 that expectation to be consistent across all types than to have to
 make special rules.


It's better to be explicit about which version of the argument you're
referring to. Make it mandatory to write x.in and x.out. Then the
compiler can catch the cases where you wrote x.in but there is no
obvious way to implement it for a ref argument. Better have a
compile-time error than a runtime bug where you think x refers to x.in
but it actually refers to x.out.



The out-contract is very useful, because it tells the user exactly
how the function will modify its argument, and what relation the
final value has to the original value. Currently, however, we don't
have .out syntax, so the above contract is inexpressible. Worse yet,
in the current implementation, we may write:

	void sqrtInPlace(ref real x)
	in { assert(x >= 0.0); }
	out {
		// Does this x refer to the initial value of x, or the
		// final value?
		assert(x >= 0.0);

		// It sure looks like the initial value to me. Which
		// makes it totally pointless. But it actually refers to
		// the final value, which is non-obvious, and also of
		// limited benefit since we can't express a more
		// definite guarantee about its final value w.r.t. its
		// original value (i.e., that the final value squared
		// equals the original value up to a given precision).
	}
	body { ... }


 
 I get the visual convenience of it, but the ambiguities around
 reference types, pointers, etc. suggest to me that it just can't be
 that simple.


OK, so we should make x.in and x.out mandatory syntax, and deprecate
straight references to unqualified x. That way, the above ambiguous code
will be rejected, and you will be forced to write in unambiguously.



Is there really any technical cost to allowing the out-contract to
address internal function variables, if the programmer wants it?


There is no cost -- it currently already lets you do that. :)


 
 ... but you can't have "x in the out-contract means x on function
 entry" without breaking that possibility.


This issue is fixed if we make x.in and x.out mandatory.



But it's also useless, because then there is no benefit to using an
out-contract as opposed to a plain old assert before the return
statement. In terms of the final executable code, there is basically
no advantage that an out-contract offers above an in-body assert
statement.  The added value of an out-contract is the documented (and
runtime-checked) guarantee it provides to the users of the API.
Referencing implementation details that the users of the API don't
care about, such as local variables in the out-contract, invalidates
this benefit, which makes it useless.


 
 I get the conceptual and self-documenting elegance of it, I just
 think that it's a false elegance when you consider the special cases
 you'd have to work round.
 
     void foo(int *x)
       in { assert *x >= 0.0; }
      out { assert *x >= 0.0; }
     body { ... }
 
 What's the "instinctive" understanding of what this means, in this
 case?  What's the sensible default behaviour?


I'd say this is a good argument for making x.in and x.out mandatory
syntax. Then it becomes clear and readable:

	void foo(int *x)
	 in { assert(*x.in >= 0.0; }
	out { assert(*x.out >= 0.0; }
	body { ... }

And for moving non-contract asserts (i.e. those that check
implementation sanity rather than make any guarantees of interest to the
caller) into the function body rather than putting them in the
out-contract.


T

-- 
Живёшь только однажды.
Sep 20 2013
parent reply "monarch_dodra" <monarchdodra gmail.com> writes:
On Friday, 20 September 2013 at 16:38:36 UTC, H. S. Teoh wrote:

 True. I agree that redefining plain "x" to mean "initial value 
 of x"
 would be difficult to implement for ref arguments


I think it would be wrong to boot. "ref" is an indirect type, 
like a pointer. Changes made to "it" (eg the reference'd value) 
*need* to be seen in the out contract. I don't think it makes 
sense to talk about "the old value of the reference". That'd be 
like asking for the old value of what a pointer was pointing to.
Sep 20 2013
parent reply Joseph Rushton Wakeling <joseph.wakeling webdrake.net> writes:
On 20/09/13 18:50, monarch_dodra wrote:

 I think it would be wrong to boot. "ref" is an indirect type, like a pointer.
 Changes made to "it" (eg the reference'd value) *need* to be seen in the out
 contract. I don't think it makes sense to talk about "the old value of the
 reference". That'd be like asking for the old value of what a pointer was
 pointing to.


Yup.  But this is why I think it makes sense for a variable x in the 
out-contract to always mean "the final value of x at the end of the function". 
If _for reference types_ the out-contract sees the changed value, that should
be 
true for all types, otherwise it's an inconsistency that is going to bite
people.

Then, in addition, you should be able to have an explicit request (x.in, x.old 
...) for the initial value (as you needed in your contract).
Sep 20 2013
parent reply "monarch_dodra" <monarchdodra gmail.com> writes:
On Friday, 20 September 2013 at 18:14:44 UTC, Joseph Rushton 
Wakeling wrote:

 On 20/09/13 18:50, monarch_dodra wrote:

 I think it would be wrong to boot. "ref" is an indirect type, 
 like a pointer.
 Changes made to "it" (eg the reference'd value) *need* to be 
 seen in the out
 contract. I don't think it makes sense to talk about "the old 
 value of the
 reference". That'd be like asking for the old value of what a 
 pointer was
 pointing to.


 Yup.  But this is why I think it makes sense for a variable x 
 in the out-contract to always mean "the final value of x at the 
 end of the function". If _for reference types_ the out-contract 
 sees the changed value, that should be true for all types, 
 otherwise it's an inconsistency that is going to bite people.

 Then, in addition, you should be able to have an explicit 
 request (x.in, x.old ...) for the initial value (as you needed 
 in your contract).


I disagree. Isn't the entire point of "pass by value" to mean "I 
operate on a copy, so you won't see any difference to the 
argument afterwards" and ref to mean "I operate on the original 
object, so all differences I make you will see"?

I think it is wrong to think in terms of "orginal/final" to begin 
with. The "out" contract should simply see what the caller sees. 
If the function body mutates something the caller doesn't see, 
than neither should the out contract.

The notion of "old"/"new" or "in"/"out" feels strange to me. It's 
making a lot of special cases for something that should really be 
very simple to begin with.
Sep 20 2013
parent reply Joseph Rushton Wakeling <joseph.wakeling webdrake.net> writes:
On 20/09/13 20:21, monarch_dodra wrote:

 I disagree. Isn't the entire point of "pass by value" to mean "I operate on a
 copy, so you won't see any difference to the argument afterwards" and ref to
 mean "I operate on the original object, so all differences I make you will
see"?

 I think it is wrong to think in terms of "orginal/final" to begin with. The
 "out" contract should simply see what the caller sees. If the function body
 mutates something the caller doesn't see, than neither should the out contract.


I get the concept, but I find it unattractive in practice just because it means 
you have different variables being treated differently in the out-contract 
depending on whether they are references or values.

I think that consistency of how variables are treated in the out-contract is 
probably going to turn out less problematic than a theoretically ideal
situation 
where the contract addresses what the outside user can/should be able to "see".

But I accept that I may be influenced by the fact that I'm used to working in 
open-source situations where the body of a function is always available if you 
really want to look at it.  If you're looking at it purely on the basis of an 
interface or a function declaration, I can understand why your concept might 
seem preferable.


 The notion of "old"/"new" or "in"/"out" feels strange to me. It's making a lot
 of special cases for something that should really be very simple to begin with.


Well, I think it's inescapable that in different circumstances you are going to 
want the out-contract to be able to access either the initial or the final
value 
of a particular variable.  Preventing the programmer from doing one or the
other 
seems an unnecessary restriction.

As Paolo has pointed out, it's in keeping with how contracts were originally 
defined.
Sep 20 2013
parent "Dicebot" <public dicebot.lv> writes:
On Friday, 20 September 2013 at 18:34:18 UTC, Joseph Rushton 
Wakeling wrote:

 I get the concept, but I find it unattractive in practice just 
 because it means you have different variables being treated 
 differently in the out-contract depending on whether they are 
 references or values.


Not really. Think about those as about variables that were passed 
to the function (and their state after function returns), not 
function parameters. Then it makes perfect sense.
Sep 20 2013
prev sibling parent Joseph Rushton Wakeling <joseph.wakeling webdrake.net> writes:
On 20/09/13 18:37, H. S. Teoh wrote:

 True. I agree that redefining plain "x" to mean "initial value of x"
 would be difficult to implement for ref arguments, and will also break
 existing code to boot. Having access to x.old is the best solution where
 possible (I'm thinking, for the sake of implementational simplicity,
 that we can restrict x.old to only work for parameters passed by value,
 since D doesn't have a generic way of cloning a reference argument).


Agree.


 No, but the current notation is ambiguous and misleading. I agree that
 x.in and x.out (or some such notation) is better.


Yes, I can go with that.  There could be a deprecation path for x => x.out if 
that's desirable, although there's precedent (as Paolo has pointed out) for 
using just x.


 I would rather say that it's illegal to refer to plain 'x' in an
 out-contract because it's ambiguous. It should always refer to either
 x.in or x.out. (Of course, we can silently still support the current
 syntax in order to preserve backward compatibility, but I'd really
 prefer it to be deprecated.)


Sure.


 This issue is fixed if we make x.in and x.out mandatory.


Agree, and I was never arguing against that.


 I'd say this is a good argument for making x.in and x.out mandatory
 syntax. Then it becomes clear and readable:

 	void foo(int *x)
 	 in { assert(*x.in >= 0.0; }
 	out { assert(*x.out >= 0.0; }
 	body { ... }

 And for moving non-contract asserts (i.e. those that check
 implementation sanity rather than make any guarantees of interest to the
 caller) into the function body rather than putting them in the
 out-contract.


In this case, yes, you can reliably handle it with in/out syntax.  It becomes 
problematic if x is a more complex data type, e.g. a class with many 
reference-type members (arrays, other classes, ...).  As there's no way to 
reliably do a deep copy of such an entity (and of course you might have
entities 
such as input ranges where you really can't preserve the state), there are 
always going to be function inputs where you can't readily access x.in in the 
out-contract.
Sep 20 2013