Design by Contract != Runtime Assertion

[Walter Bright]

bearophile wrote:
> To me those lines look more like math formulas than normal D code.

This makes no sense to me. Programming languages *are* math. There is no "more 
like math".


> This is useful because the contract code needs to be as much bug-free as
> possible, otherwise the contracts don't help. The short syntax helps the eye
> see that the code is correct, and having a declarative style this probably
> helps the analyser too. In D you need loops, sets, and other things there,
> that I think are less easy to analyse (because it is possible to analyse
> them, because commercial Lints for C are probably able to do it).

Again, this makes no sense. Furthermore, as I've attempted to explain before, 
doing automated analysis on loops, etc., is well-trod and well-understood 
territory. It's 1970's technology.



>> Spec# does not do proper inheritance of preconditions (they cannot be
>> weakened). It missed half of what dbc is all about with polymorphism.
> It seems you and me are both blind: you see only the downsides of Spec# and I
> see only the good sides of it.

I suggest Meyer's epic tome "Object-Oriented Software Construction" for the 
rationale and theory behind dbc. Once you have, it's pretty obvious where these 
well-designed languages completely missed the boat on dbc. Every one of them 
(except Eiffel, of course) punted on contract inheritance, which is inexcusable 
in a language that is centered around polymorphism and inheritance.

Dbc without contract inheritance is nothing more than an assert. NOTHING more.


> I don't know why they have taken those
> decisions. Maybe to allow the static verifiability.

Getting rid of polymorphic behavior to enhance static verifiability doesn't make 
much sense in an OOP language.



>> C# missed the boat on polymorphic dbc completely.
> 
> They have decided that it's better to not change the C# language to add DbC
> to it, so they have implemented DbC as a library only (but it contains a
> simplified static analyser too), so I think they have had constraints.

I.e. they missed the boat. It is not dbc. (And Microsoft has exhibited no 
reluctance to add features to the C# language, so this makes no sense either.)

Frankly, because of contract inheritance, you cannot implement dbc without 
language changes.


>> Spec# generates code for and checks its contracts at runtime.
> Right, because there are external libs that may not use contracts, etc. But
> it tests the contracts at compile-time too where possible.

That's not what I read about it.


>> And lastly, please demonstrate how: ... is not. Because I cannot figure out
>> where you uncovered a problem.
> You are right, in simple cases it's the same thing. Maybe for a good enough
> static analyser it's the same thing for more complex cases too, that contains
> nested loops, etc.

As I've repeatedly said, loops are not a problem for data flow analysis. If a 
static analyzer is having problems with loops, I suggest mailing them a book on 
how to write compilers instead of blaming the language.