Design by Contract != Runtime Assertion

[Walter Bright]

bearophile wrote:
> But the style normal D contracts are written doesn't lead to a simple
> analysis. In Spec# and Eiffel and Spark they use specific constructs inside
> contracts, that look more like math,

look more like math???


> they help static verifiers. I have
> uncovered and reported here this problem some weeks ago, but it was ignored.
> People aren't seeing it as problem yet, it's an invisible problem still. So
> so far there is really no interest even in making the job of static D
> verifiers easer.

Spec# does not do proper inheritance of preconditions (they cannot be weakened). 
It missed half of what dbc is all about with polymorphism. C# missed the boat on 
polymorphic dbc completely.

Spec# generates code for and checks its contracts at runtime.

And lastly, please demonstrate how:

     requires a == b;

is checkable with a static verifier and:

     assert(a == b);

is not, and how:

     static assert(a == b);

is not. Because I cannot figure out where you uncovered a problem.