I read that compiler can enforce dbc at compile time.. How does it do it?
R – Compile time checking in Design by Contract
design-by-contract
Related Solutions
The main problem with DBC is that in the vast majority of cases, either the contract cannot be formally specified (at least not conveniently), or it cannot be checked with current static analysis tool. Until we get past this point for mainstream languages (not Eiffel), DBC will not give the kind of assurance that people need.
In TDD, tests are written by a human being based on the current natural-text specifications of the method that are (hopefully) well-documented. Thus, a human interprets correctness by writing the test and gets some assurance based on that interpretation.
If you read Sun's guide for writing JavaDocs, it says that the documentation should essentially lay out a contract sufficient to write a test plan. Hence, design by contract is not necessarily mutually exclusive with TDD.
The PEP you found hasn't yet been accepted, so there isn't a standard or accepted way of doing this (yet -- you could always implement the PEP yourself!). However, there are a few different approaches, as you have found.
Probably the most light-weight is just to simply use Python decorators. There's a set of decorators for pre-/post-conditions in the Python Decorator Library that are quite straight-forward to use. Here's an example from that page:
>>> def in_ge20(inval):
... assert inval >= 20, 'Input value < 20'
...
>>> def out_lt30(retval, inval):
... assert retval < 30, 'Return value >= 30'
...
>>> @precondition(in_ge20)
... @postcondition(out_lt30)
... def inc(value):
... return value + 1
...
>>> inc(5)
Traceback (most recent call last):
...
AssertionError: Input value < 20
Now, you mention class invariants. These are a bit more difficult, but the way I would go about it is to define a callable to check the invariant, then have something like the post-condition decorator check that invariant at the end of every method call. As a first cut you could probably just use the postcondition decorator as-is.
Best Answer
As far as I know, the most powerful static DbC language so far is Spec# by Microsoft Research. It uses a powerful static analysis tool called Boogie which in turn uses a powerful Theorem Prover / Constraint Solver called Z3 to prove either the fulfillment or violation of contracts at design time.
If the Theorem Prover can prove that a contract will always be violated, that's a compile error. If the Theorem Prover can prove that a contract will never be violated, that's an optimization: the contract checks are removed from the final DLL.
As Charlie Martin points out, proving contracts in general is equivalent to solving the Halting Problem and thus not possible. So, there will be a lot of cases, where the Theorem Prover can neither prove nor disprove the contract. In that case, a runtime check is emitted, just like in other, less powerful contract systems.
Please note that Spec# is no longer being developed. The contract engine has been extracted into a library, called Code Contracts for .NET, which will be a part of .NET 4.0 / Visual Studio 2010. However, there will be no language support for contracts.