On the Duality between Vacuity and Coverage
Orna Kupferman, Wenchao Li, Sanjit A. Seshia · 2008
Abstract. Sanity checks such as vacuity and coverage are used to evaluate the quality of both implementations and specifications. We study vacuity and coverage in a setting in which both the implementation and the specification are given by circuits, at different levels of abstraction. We show that, in this setting, the two notions are dual. To formalize this duality, we study a wide range of mutations that one can apply to a circuit and partition them into mutations that add, remove, and modify behaviors. Many mutations correspond to actual faults, such as ones in which signals are ignored, flipped, delayed, or stuck at a value, and combinations thereof. We introduce and study the notion of dual mutations. A mutation µ that adds or modifies behaviors is dual to a mutation ˜µ that removes or modifies behaviors if, for all implementations I and specifications S, satisfaction of S by a mutant implementation Iµ, obtained from I by applying µ, is related to satisfaction by I of a mutant specification S˜µ, obtained from S by applying ˜µ. Thus, the low coverage of I by S, which causes Iµ to satisfy S, is related to the vacuous satisfaction of S in I, which causes I to satisfy S˜µ. Beyond the clean theoretical picture that the duality suggests, it offers two important applications. First, we obtain new coverage metrics and new definitions of vacuity that have so far been used only in one of the sanity checks. Second, when low coverage is detected with a mutation, a tighter specification can be automatically obtained by applying its dual mutation to the original specification. 1