TDD using DBC

Test Driven Development using Design by Contract

TDD

Test-Driven Development Cycle in general involves these steps:

1. Write the test
2. Write the code
3. Run the automated test
4. Refactor
5. Repeat

This is a laudable process to aspire to. The problem is that unit testing is time-consuming and arduous without help. For Java developers using Eclipse as their IDE, there is a solution (read on).

Note: A good book on TDD is Agile Java by Langr.

DBC

Design by Contract has a history that goes back to the 1980s with work by Bertrand Meyer. The primary pragmatic idea we will use today is the concept of an assertion. There are three types of assertions:

1. Precondition
2. Postcondition
3. Invariant

The goal is to specify business rules that must be enforced for the services to take place.

Precondition

A precondition is a condition that must hold true before a method can be executed. The format is:

@pre (boolean expression)

Examples

• @pre !isCancelled()
  This might be used to make sure an Order can be modified.
  

• @pre quantityOrdered > 0
  This might be used to make sure an amount being Ordered is a positive integer.

Postcondition

A postcondition is a condition that must hold true after a method is executed. The format is:

@post (boolean expression)

Examples

• @post ($ret == (inventory.contains(aProduct))
  This can be read as "answer whether my inventory contains a product". It may be an assertion on the Business.sells( aProduct ) method.
  

• @post savingsAcct.getBalance() == $pre(savingsAcct.getBalance()) - anAmount
  This business rule checks to make sure that after the SavingsAccount.withdraw( anAmount ) method that the balance is debited correctly.

Invariant

An invariant is a condition that must always hold true for a class. The format is:

@inv (boolean expression)

Examples

• @inv balance >= 0.0
  This would certainly be a rule for Accounts in a banking application.
  

• @inv number.length() == 9
  This would be a rule for a SocialSecurityNumber class.
  

Development Process using TDD and DBC

To use the assertions we've been discussing, put them in as comments into your modeling tool or in JavaDocs in your IDE.

Alright - that's a lot of information to digest before actually doing anything productive. In my next post, I'll introduce a tool to automate much of the heavy lifting, making TDD a real possibility on your project.