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

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

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

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

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

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

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.

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.

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

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