View mode: basic / threaded / horizontal-split · Log in · Help
August 01, 2010
A problem with D contracts
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
August 01, 2010
Re: A problem with D contracts
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
August 01, 2010
Re: A problem with D contracts
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
August 01, 2010
Re: A problem with D contracts
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
August 01, 2010
Re: A problem with D contracts
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
August 01, 2010
Re: A problem with D contracts
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
August 01, 2010
Re: A problem with D contracts
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.
August 01, 2010
Re: A problem with D contracts
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.
August 01, 2010
Re: A problem with D contracts
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
August 01, 2010
Re: A problem with D contracts
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
« First   ‹ Prev
1 2 3
Top | Discussion index | About this forum | D home