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

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

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


 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.


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

 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

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


This can be done with array op

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