Design by Contract != Runtime Assertion

[bearophile]

%u:

> It is said that D supports Design by Contract (DbC) programming, when in fact
> what it has is runtime assertions. There is, however, a big difference. DbC
> necessarily means that a compiler would have a theorem prover and would need
> to prove at /Compile/-time whether or not an expression can be satisfied
> (similar to what is done in the Spec# language by Microsoft Research), because
> the name is /Design/ by contract. It is not the same as assertions, which
> occur at run time.

>From what I have read of DbC it is acceptable to call it DbC even if the enforcements are done at run time.

Having the tests done at compile time as in Spec# and Spark is a nice thing, but it requires a constraint solver inside the compiler, that Walter doesn't seem interested in (and it probably requires a more rigid way of writing code).


> I was wondering if actual design-by-contract programming (rather than mere
> assertions) will be available in D at a later time?

If D becomes widespread, then sooner or later someone will surely try to write an external constraint solver to try to verify the assertions at compile time.

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, 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.

Bye,
bearophile