Tool Support for Test-Driven Development Using Formal Specifications
This paper describes how Test-Driven Development (TDD) can be conducted using formal specifications with appropriate tool support. In TDD, the test code is a formal documentation of the required behaviour of the component or system that is being developed, but this documentation is necessarily incomplete and often over-specific. The authors propose an alternative approach to TDD that is to develop the specification of the required behaviour in a formal notation as a part of the TDD process and to generate test oracles from that specification. This approach has the advantage that the specifications can be complete and appropriately abstract but still support TDD.