A Formal Analysis of Iterated TDD

TL;DR

This paper provides a formal analysis of iterated Test Driven Development (TDD), identifying conditions under which it produces correct and stable code, and explaining why previous research results vary.

Contribution

It formalizes iterated TDD and identifies a specific context where it guarantees correct, stable code, clarifying inconsistent prior findings.

Findings

Iterated TDD can provably produce correct code within certain contexts.

Outside the context, iterated TDD exhibits chaotic, unpredictable behavior.

Previous research results are explained by whether the context was present or absent.

Abstract

In this paper we formally analyze the software methodology called (iterated) Test Driven Development (TDD). We formally define Specification, Software, Testing, Equivalence Partitions, Coupling, to argue about the nature of the software development in terms of TDD. We formalize Iterative TDD and find a context in which iterated TDD ``provably produce'' ``provably correct code'' from ``specifications'' while being stable in terms of iterated code churns. We demonstrate that outside this context iterated TDD will exhibit chaotic behavior, implying unpredictable messy amount of code churn. We argue that the research finding of ``ineffective'' iterated TDD found by earlier researches are due to missing this context, while the findings of ``effective'' iterated TDD is due to accidentally falling into the context or simply placebo.