Test-Driven Development with Oracles and Formal Specifications

The current industry trend to using Test Driven Development (TDD) is a recognition of the high value of creating executable tests as part of the development process. In TDD, the test code is a formal documentation of the required behaviour of the component or system being developed, but this documentation is necessarily incomplete and often over-specific. An alternative approach to TDD 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. In this thesis we present tools in support of this approach that allow formal specifications to be written in a readable manner that is tightly integrated with the code through an integrated development environment, and test oracles to be generated automatically. The generated test code integrates smoothly with test frameworks (e.g., JUnit) and so can be directly used in TDD. This approach has the advantage that the specifications can be complete and appropriately abstract but still support TDD.