Assertion-Driven Development: Assessing the Quality of Contracts Using Meta-Mutations

Agile development methods have gained momentum in the last few years and, as a consequence, test-driven development has become more prevalent in practice. However, test cases are not sufficient for producing dependable software and we rather advocate approaches that emphasize the use of assertions or contracts over that of test cases. Yet, writing self-checks in code has been shown to be difficult and is itself prone to errors. A standard technique to specify runtime properties is design-by contract(DbC). But how can one test if the contracts themselves are sensible and sufficient? We propose a measure to quantify the goodness of contracts (or assertions in a broader sense). We introduce meta-mutations at the source code level to simulate common programmer errors that the self-checks are supposed to detect. We then use random mutation testing to determine a lower and upper bound on the detectable mutations and compare these bounds with the number of mutants detected by the contracts. Contracts are considered ldquogoodrdquo if they detect a certain percentage of the detectable mutations.We have evaluated our tools on Java classes with contracts specified using the Java Modeling Language (JML). We have additionally tested the contract quality of 19 implementations, written independently by students, based on the same specification.