Test Case Generation by Contract Mutation in Spec#

Publication Type:

Conference Paper


MBT 2009, Elsevier B.V., Volume 253, York, p.71-86 (2009)


Mutation testing is a well known fault-based testing technique that is normally used to assess the quality of a test suite. In this paper we use the mutation operation to derive test cases that demonstrate the absence of certain faults in an implementation: In difference to conventional mutation testing, which mutates program code, we mutate program contracts and generate test-input data that is able to distinguish the mutated contract from the original one. We show how existing development tools can be used as a foundation for the presented methodology: In particular we rely on the counter-example generation capabilities of the Spec#/Boogie/Z3 system.