Design-by-contract is a light-weight formal development paradigm, in which object-oriented software is specified with so-called software contracts. Contracts are annotations in the source code that explicitly document intended functional behavior and can be used for verifying correctness of a particular implementation or as test oracles during automatic test case generation. As writing strong specifications is an expensive and error-prone activity due to lack of expertise and tool support, developers are often only willing to write simpler specifications, covering only a fraction of all functional properties. As a consequence, software quality is lowered, or even worse, potential bugs remain undetected during software verification. To give developers a sense of specification coverage, we propose a methodology that considers the degree of incomplete specifications by means of mutation analysis. We consider Java programs annotated with JML and employ the deductive program verifier KeY–2.7.0 to show that this approach is applicable to numerous open-source JML projects from the literature.