Design by Contract != Runtime Assertion

Andrei Alexandrescu SeeWebsiteForEmail at erdani.org
Sun Nov 21 23:04:04 PST 2010


On 11/22/10 12:46 AM, %u wrote:
> Hello!
>
> I just became an incredibly big fan of D; it has everything I've wanted,
> except one thing:
> 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.
> I was wondering if actual design-by-contract programming (rather than mere
> assertions) will be available in D at a later time?
>
> Thank you!

Contracts based on theorem proving postdate contract programming as 
defined by Meyer by a long time, and are in fact a fairly new and active 
research topic. It would be a misrepresentation to equate theorem 
proving with contracts.

You may want to consult TDPL for a related discussion. D currently 
defines contract programming in keeping with Meyer's definition. There 
are no plans to integrate static theorem proving abilities with contracts.


Andrei


More information about the Digitalmars-d mailing list