Design by Contract != Runtime Assertion

[Jonathan M Davis]

On Sunday 21 November 2010 22:46:38 %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!

As I recall, all design by contract says is that a function has a contract 
saying that if you give it input which follows a certain set of guidelines, it 
will give you output which follows a certain set of guidelines. It says nothing 
about enforcement or proving that a function actually follows the contract. If 
you violate the contract by giving it bad data, then it's implementation-defined 
as to what happens. And obviously, if the function doesn't follow the contract, 
then it's implementation-defined as to what happens.

What D does is give you a means of making sure that a function is following the 
contract that you intended for it. pre-conditions verify that it's given 
arguments which follow the contract, post-conditions verify that the function's 
output follows the contract, and invariants help guarantee that the state of an 
object is within _its_ contract. All of it is a way to verify that the contracts 
are kept.

All DbC says is that the contracts exist. How you guarantee that they're 
followed is another matter entirely. And having pre-conditions and post-
conditions verified programmatically at runtime is a classic way to do that.

Actually doing proofs of any sort - programmatically or otherwise - can be very 
difficult, and there's no way that that sort of thing is going to make it into the 
language. It's totally unnecessary, it would be an absolute nightmare to 
implement, and now you have another source of potential error: your proof. By 
verify that the contract is followed at runtime, D has implemented the _least_ 
error-prone solution to guaranteeing that function contracts are adhered to.

- Jonathan m Davis