Writing specifications is hard. It is especially hard to write specifications that don’t leave things out (underconstrain) or say too much (overconstrain). This paper deals with two particular problems and argues that they can be tackled with the same analysis
-
Vacuity: accidentally specifying a property that says nothing because the precondition is unsatisfiable.
-
Completeness: accidentally leaving out some important property.
Recognizing that they are related allows cross-fertilization of ideas between two separate groups of researchers.
Both vacuity and coverage are defined in terms of semantic notions of mutation of subformulae (vacuity) or states. That is, if changing the value of the subformula/state makes no difference to whether a formula is satisfied, then either the formula is vacuous or the state is not covered. (Definitions 2 and 4.)
These can then be generalized to changing the value all the time (structural), exactly once (node) and N times (tree). (The tree/node terminology comes from the definition in terms of a Kripke structure.)
For both coverage and vacuity, it can be useful to produce witnesses that show how mutant implementations (slightly modified versions of the implementation) would fail to satisfy the formula.
A witness is interesting if it satisfies the specification non-vacuously.
and
In the context of coverage, however, we return to the user a family of counterexamples – one for each sub-specification that is no longer satisfied in the system with c mutated.
Generating coverage counterexamples is done by introducing two new variables for each subformula to decide whether to invert the subformula and to track how many times it has been inverted before. (This is for hardware model checking where all signals are booleans.)
Generating vacuity counterexamples is done by introducing a new variable to select which subformula to invert and then solving for the choice that makes no difference.
The paper is written from the context of model checking, temporal logic and hardware verification but may be more general than that.