www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - A problem with D contracts

reply bearophile <bearophileHUGS lycos.com> writes:
D contract programming lacks the 'old', but there is another different problem.

Allowing only asserts (and calls to only pure/readonly functions) in
precoditions, postconditions and invariants opens the door for future software
that perform automatic compile-time verification of contracts.

Putting all kind of D code inside contracts will make them very hard to
statically verify.

But simple asserts sometimes are not enough to test more complex things. So
other more serious contract systems allow for asserts that contain forall, max,
min, sets, and few more simple things, this is an example from a system for
Java:

/*  assert (\forall int i; 0 <= i && i < n; a[i] != null);

Beside keeping the door open to future automatic verification, that short style
for conditions helps keep them shorter and less buggy (also because it helps
psychological 'chunking'). If code inside contracts is long and complex then it
too can contain bugs.

Bye,
bearophile
Jul 31 2010
next sibling parent reply Jonathan M Davis <jmdavisprog gmail.com> writes:
On Saturday 31 July 2010 18:33:09 bearophile wrote:
 D contract programming lacks the 'old', but there is another different
 problem.
 
 Allowing only asserts (and calls to only pure/readonly functions) in
 precoditions, postconditions and invariants opens the door for future
 software that perform automatic compile-time verification of contracts.
 
 Putting all kind of D code inside contracts will make them very hard to
 statically verify.

D strives to be practical and useful rather than perfect - not to mention what's best here depends on your goals. IIRC TDPL, specifically mentions that contracts allow for I/O for debugging purposes. Requiring contracts to be pure would destroy that ability, and there plenty of situations where that would be a big problem. Also, while automatic compile-item verification of contracts might be cool, you're talking about a future extension that would likely be used by a small percentage of the D user base while I'm willing to be that the ability to put print statements and the like in contracts would be used by a far greater percentage. So, while I can see why purity for contracts could be useful, what we have does the job, and enforcing purity has serious downsides. Personally, I think that what we have works quite well, and it's way better than the situation in any other language that I've used. - Jonathan M Davis
Jul 31 2010
next sibling parent Marianne Gagnon <auria.mg gmail.com> writes:
Agreed, and if static verification is ever implemented (like there isn't
already enough to do on D ;) I can very well imagine adding contract blocks
with the "pure" keyword (or is it an annotation now?)

 On Saturday 31 July 2010 18:33:09 bearophile wrote:
 D contract programming lacks the 'old', but there is another different
 problem.
 
 Allowing only asserts (and calls to only pure/readonly functions) in
 precoditions, postconditions and invariants opens the door for future
 software that perform automatic compile-time verification of contracts.
 
 Putting all kind of D code inside contracts will make them very hard to
 statically verify.

D strives to be practical and useful rather than perfect - not to mention what's best here depends on your goals. IIRC TDPL, specifically mentions that contracts allow for I/O for debugging purposes. Requiring contracts to be pure would destroy that ability, and there plenty of situations where that would be a big problem. Also, while automatic compile-item verification of contracts might be cool, you're talking about a future extension that would likely be used by a small percentage of the D user base while I'm willing to be that the ability to put print statements and the like in contracts would be used by a far greater percentage. So, while I can see why purity for contracts could be useful, what we have does the job, and enforcing purity has serious downsides. Personally, I think that what we have works quite well, and it's way better than the situation in any other language that I've used. - Jonathan M Davis

Jul 31 2010
prev sibling next sibling parent reply bearophile <bearophileHUGS lycos.com> writes:
Jonathan M Davis:

 So, while I can see why purity for contracts could be useful, what we have
does 
 the job, and enforcing purity has serious downsides.

You have missed half (well, two thirds) of what I was trying to say. It's not just about enforcing purity (or just readonly of names in outer scopes), but it's also a problem of automatic analysis of notation (code). If you have generic D code it's harder to perform inferences on it. That's the purpose of those forall, etc, I have tried to talk about (and maybe you have also missed the part about the relation between code size and bug-prone nature of contracts). Automatic verification of contracts is an important feature, that can be made much harder (or impossible) to implement if contract contents aren't clean and simple. Putting print statements inside contracts is just wrong. As in future probably a second documentation system will be added/used to/in D, a second unit-testing system too, probably eventually a second contract system too will be added/used, because the built-in ones are not designed in a serious way, all three of them are just toys :-) "keeping their usage simple" doesn't hold when they lack essential features (I have discussed about missing parts in unittest system recently). Bye, bearophile
Jul 31 2010
next sibling parent reply Walter Bright <newshound2 digitalmars.com> writes:
bearophile wrote:
 You have missed half (well, two thirds) of what I was trying to say. It's not
 just about enforcing purity (or just  readonly of names in outer scopes), but
 it's also a problem of automatic analysis of notation (code). If you have
 generic D code it's harder to perform inferences on it. That's the purpose of
 those forall, etc, I have tried to talk about (and maybe you have also missed
 the part about the relation between code size and bug-prone nature of
 contracts).

It is not easier to statically analyze a forall rather than a foreach. I also see no evidence that foreach is more bug-prone than a forall would be.
Jul 31 2010
parent reply bearophile <bearophileHUGS lycos.com> writes:
Walter Bright:
 It is not easier to statically analyze a forall rather than a foreach.

The problem is that you can put any kind of code inside D contracts, this will make them them very to analyse automatically. The restricted semantics is a way to avoid this.
 I also see no evidence that foreach is more bug-prone than a forall would be.

I have used Python lazy/eager list comps, and I think they decrease bug-count and speed-up coding. In the past I have explained why (mostly because of psychological chunking). Bye, bearophile
Aug 01 2010
parent Walter Bright <newshound2 digitalmars.com> writes:
bearophile wrote:
 Walter Bright:
 It is not easier to statically analyze a forall rather than a foreach.

The problem is that you can put any kind of code inside D contracts, this will make them them very to analyse automatically. The restricted semantics is a way to avoid this.

All it means is the analysis returns one of three states: 1. yes 2. no 3. couldn't figure it out This is normal for static analysis. Optimizers use it extensively, for example.
 I also see no evidence that foreach is more bug-prone than a forall would
 be.

I have used Python lazy/eager list comps, and I think they decrease bug-count and speed-up coding. In the past I have explained why (mostly because of psychological chunking).

Supporting list comprehensions is a separate issue from whether foreach should be disallowed in contracts because comps are better.
Aug 01 2010
prev sibling parent reply godworshipper <worship deity.org> writes:
bearophile Wrote:

 because the built-in ones are not designed in a serious way, all three of them
are just toys :-)

That's blasphemy! I thought you believed in D :-(
Aug 01 2010
parent bearophile <bearophileHUGS lycos.com> writes:
godworshipper:
 That's blasphemy! I thought you believed in D :-(

I think I lost my temper a bit while answering Jonathan, I am sorry Jonathan. Bye, bearophile
Aug 01 2010
prev sibling next sibling parent bearophile <bearophileHUGS lycos.com> writes:
Jonathan M Davis:

 and it's way better than the situation in any 
 other language that I've used.

I think you need to raise your expectations a bit, you have to design a language that will be 'good enough' ten years from now, not a language that is 'good' compared to languages designed fifteen years ago or more :-) Bye, bearophile
Jul 31 2010
prev sibling parent reply bearophile <bearophileHUGS lycos.com> writes:
Jonathan M Davis:
 IIRC TDPL, specifically mentions that contracts 
 allow for I/O for debugging purposes.

I have not yet read that part. I see print statements (and exceptions) inside contracts as something to kill with fire in my code. What's the purpose of printing stuff in contracts? Maybe Andrei is mistaken here.
 Requiring contracts to be pure would 
 destroy that ability, and there plenty of situations where that would be a big 
 problem.

See also enhancement request 3856 Bye, bearophile
Aug 01 2010
parent Walter Bright <newshound2 digitalmars.com> writes:
bearophile wrote:
 Jonathan M Davis:
 IIRC TDPL, specifically mentions that contracts allow for I/O for debugging
 purposes.

I have not yet read that part. I see print statements (and exceptions) inside contracts as something to kill with fire in my code. What's the purpose of printing stuff in contracts?

Debugging support, as mentioned in TDPL. Being able to pepper one's code with print statements to find out where it goes wrong is an INCREDIBLY useful debugging technique.
Aug 01 2010
prev sibling next sibling parent Jonathan M Davis <jmdavisprog gmail.com> writes:
On Saturday 31 July 2010 19:47:10 bearophile wrote:
 Automatic verification of contracts is an important feature, that can be
 made much harder (or impossible) to implement if contract contents aren't
 clean and simple. Putting print statements inside contracts is just wrong.
 As in future probably a second documentation system will be added/used
 to/in D, a second unit-testing system too, probably eventually a second
 contract system too will be added/used, because the built-in ones are not
 designed in a serious way, all three of them are just toys :-) "keeping
 their usage simple" doesn't hold when they lack essential features (I have
 discussed about missing parts in unittest system recently).

Actually, truth be told, I wouldn't consider automatic verification to be all that important at all - particularly because it would be so hard to do ands so few people would likely use it. I totally agree that it would be a good feature, but I doubt that it's one that will ever materialize - or if it does it won't be any time soon. Besides, if you assume that contracts are pure or have something that verifies that they are, then you could still do those checks. Enforcing purity would be a serious impairment. Putting print statements in contracts for debugging purposes is a major and positive feature. Now, I agree that outside of debugging a problem print statements have no business in contracts - they certainly shouldn't stay there longterm - but it would impair debugging to disallow them. I really don't understand what your problem with contracts or unit testing is. What we have works quite well. I'm sure that it could be improved, but it works well. And honestly, I don't see automatic verification as being particularly practical or useful any time soon - not to mention that it wouldn't be all that hard for you to have assertions in there that couldn't be verified statically anyway. What we currently have is extremely practical and does its job. What we have in D is a major step forward, and with D2 stabilizing, you're not going to get it changed in any big way. And in this particular case, I really don't think that you're going to win any arguments - certainly not with folks like Walter or Andrei. Purity in contracts is definitely not one of the goals, and IIRC it has been explicitly stated by Walter and/or Andrei that enforcing purity in contracts would be bad for D. - Jonathan M Davis
Jul 31 2010
prev sibling next sibling parent reply Walter Bright <newshound2 digitalmars.com> writes:
bearophile wrote:
 But simple asserts sometimes are not enough to test more complex things. So
 other more serious contract systems allow for asserts that contain forall,
 max, min, sets, and few more simple things, this is an example from a system
 for Java:
 
 /*  assert (\forall int i; 0 <= i && i < n; a[i] != null);

This does not make it simpler, it just makes things more complicated by now having two ways to do a foreach.
Jul 31 2010
parent reply bearophile <bearophileHUGS lycos.com> writes:
Walter Bright:
 /*  assert (\forall int i; 0 <= i && i < n; a[i] != null);

This does not make it simpler, it just makes things more complicated by now having two ways to do a foreach.

The point here is to restrict a lot the kind of code and instructions you can put inside contracts, so eventually you will have a chance to test them automatically. When you have copied Eiffel to design D contracts you probably have seen that in Eiffel you can't put arbitrary code inside contracts (the same is true for contract systems in C# and Java, here it's D that is designed in the wrong way). This is a limit that was there because otherwise it kills the possibility of enforcing them statically. Bye, bearophile
Aug 01 2010
next sibling parent Walter Bright <newshound2 digitalmars.com> writes:
bearophile wrote:
 Walter Bright:
 /*  assert (\forall int i; 0 <= i && i < n; a[i] != null);

having two ways to do a foreach.

The point here is to restrict a lot the kind of code and instructions you can put inside contracts, so eventually you will have a chance to test them automatically.

Replacing foreach with another looping construct does absolutely nothing to enhance analyse-ability. You could replace them with a rat's nest of goto's and the compiler can still figure it out using standard, well known algorithms. dmd's global optimizer is an example of this. In fact, all structured statements are reduced to if's and goto's before handing them to the optimizer, and the optimizer reconstructs all the loops, etc., from that flow graph. It's 1970's technology <g>.
 When you have copied Eiffel to design D contracts you probably have seen that
 in Eiffel you can't put arbitrary code inside contracts (the same is true for
 contract systems in C# and Java, here it's D that is designed in the wrong
 way). This is a limit that was there because otherwise it kills the
 possibility of enforcing them statically.

No, it doesn't kill it at all. It only kills it for *some* contracts.
Aug 01 2010
prev sibling parent Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
On 08/01/2010 07:04 AM, bearophile wrote:
 Walter Bright:
 /*  assert (\forall int i; 0<= i&&  i<  n; a[i] != null);

This does not make it simpler, it just makes things more complicated by now having two ways to do a foreach.

The point here is to restrict a lot the kind of code and instructions you can put inside contracts, so eventually you will have a chance to test them automatically. When you have copied Eiffel to design D contracts you probably have seen that in Eiffel you can't put arbitrary code inside contracts (the same is true for contract systems in C# and Java, here it's D that is designed in the wrong way). This is a limit that was there because otherwise it kills the possibility of enforcing them statically.

I think D made the right choice here. The space of contracts that can be effectively checked during compilation is very small, and the relative complexity of the checkers is very high. (Array bounds checking is a classic example.) Restricting contracts to make them statically checkable with today's technology would essentially push them out of existence. Andrei
Aug 01 2010
prev sibling next sibling parent KennyTM~ <kennytm gmail.com> writes:
On Aug 1, 10 09:33, bearophile wrote:
 D contract programming lacks the 'old', but there is another different problem.

 Allowing only asserts (and calls to only pure/readonly functions) in
precoditions, postconditions and invariants opens the door for future software
that perform automatic compile-time verification of contracts.

 Putting all kind of D code inside contracts will make them very hard to
statically verify.

That's too restrictive. If the goal is to verify statically (verify at compile time), then allow all CTFE-able code, not just asserts + pure functions.
 But simple asserts sometimes are not enough to test more complex things. So
other more serious contract systems allow for asserts that contain forall, max,
min, sets, and few more simple things, this is an example from a system for
Java:

 /*  assert (\forall int i; 0<= i&&  i<  n; a[i] != null);

Even if only assert is allowed in the outermost level, I don't see why \forall is needed. assert(reduce!"a&&b"(map!"a!=null"(a[0..n]))) but both are not simpler than foreach (i; 0..n) assert(a[i] != null); (BTW, there should be an 'all = reduce!"a&&b"' and 'any = reduce!"a||b"' in std.algorithm, but short-circuited.)
 Beside keeping the door open to future automatic verification, that short
style for conditions helps keep them shorter and less buggy (also because it
helps psychological 'chunking'). If code inside contracts is long and complex
then it too can contain bugs.

 Bye,
 bearophile

Aug 01 2010
prev sibling next sibling parent Kagamin <spam here.lot> writes:
bearophile Wrote:

 /*  assert (\forall int i; 0 <= i && i < n; a[i] != null);
 

assert(a[0..n].notSame(null));
Aug 01 2010
prev sibling next sibling parent reply Norbert Nemec <Norbert Nemec-online.de> writes:
I agree that contracts offer too much liberty. However, I would actually 
go one step further than bearophile:

I find the need for "assert" statements not only superfluous but 
actually misleading. A contract violation is something conceptionally 
different from a broken assertion. Assertions and contracts have 
different purposes.

In my opinion, contracts should not be lists of statements but simply 
boolean expressions that have to evaluate to true. Contract checks would 
then become decoupled from assertion checks. Both could be switched 
independently at compile time.

For any case where the contract is more complex than what can be handled 
by an expression, one should simply define a pure function, which would 
even help to unclutter the code and keep contract short and concise to read.

Greetings,
Norbert


On 01/08/10 02:33, bearophile wrote:
 D contract programming lacks the 'old', but there is another different problem.

 Allowing only asserts (and calls to only pure/readonly functions) in
precoditions, postconditions and invariants opens the door for future software
that perform automatic compile-time verification of contracts.

 Putting all kind of D code inside contracts will make them very hard to
statically verify.

 But simple asserts sometimes are not enough to test more complex things. So
other more serious contract systems allow for asserts that contain forall, max,
min, sets, and few more simple things, this is an example from a system for
Java:

 /*  assert (\forall int i; 0<= i&&  i<  n; a[i] != null);

 Beside keeping the door open to future automatic verification, that short
style for conditions helps keep them shorter and less buggy (also because it
helps psychological 'chunking'). If code inside contracts is long and complex
then it too can contain bugs.

 Bye,
 bearophile

Aug 01 2010
parent Walter Bright <newshound2 digitalmars.com> writes:
Norbert Nemec wrote:
 I agree that contracts offer too much liberty. However, I would actually 
 go one step further than bearophile:
 
 I find the need for "assert" statements not only superfluous but 
 actually misleading. A contract violation is something conceptionally 
 different from a broken assertion. Assertions and contracts have 
 different purposes.

In what way are their purposes different?
 In my opinion, contracts should not be lists of statements but simply 
 boolean expressions that have to evaluate to true. Contract checks would 
 then become decoupled from assertion checks. Both could be switched 
 independently at compile time.
 
 For any case where the contract is more complex than what can be handled 
 by an expression, one should simply define a pure function, which would 
 even help to unclutter the code and keep contract short and concise to 
 read.

I think that's a stylistic issue, not a language one.
Aug 01 2010
prev sibling parent Jay Byrd <JayByrd rebels.com> writes:
On Sat, 31 Jul 2010 21:33:09 -0400, bearophile wrote:

 D contract programming lacks the 'old', but there is another different
 problem.

Yet another problem is that the logic is completely wrong. The preconditions that should be executed are those of the static type -- the contract is with the invoker -- not some disjunction or conjunction of conditions of the dynamic type stack. Better examples and explanations in TDPL would make this issue clear. The problems with the current implementation goes unnoticed because it is way too lenient, silently failing to impose requirements and provide guarantees. -- JB
 
 Allowing only asserts (and calls to only pure/readonly functions) in
 precoditions, postconditions and invariants opens the door for future
 software that perform automatic compile-time verification of contracts.
 
 Putting all kind of D code inside contracts will make them very hard to
 statically verify.
 
 But simple asserts sometimes are not enough to test more complex things.
 So other more serious contract systems allow for asserts that contain
 forall, max, min, sets, and few more simple things, this is an example
 from a system for Java:
 
 /*  assert (\forall int i; 0 <= i && i < n; a[i] != null);
 
 Beside keeping the door open to future automatic verification, that
 short style for conditions helps keep them shorter and less buggy (also
 because it helps psychological 'chunking'). If code inside contracts is
 long and complex then it too can contain bugs.
 
 Bye,
 bearophile

Sep 10 2010