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.
