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.
