Exhaustive coverage tries every combination of conditions in a decision and checks the correct answer for each. That is possible only where the decision is finite and deterministic, and it is the one corner where a coverage criterion stops being a reachability signal and becomes a bounded proof. Multiple-condition coverage (MCC) runs the full truth table; MC/DC (modified condition/decision coverage) is the tractable near-exhaustive substitute that safety-critical regimes mandate. Decision tables are the sibling that reaches the same exhaustiveness by authoring the table instead.

What it catches

The guarantee is a bounded soundness proof: over a finite, deterministic decision checked by a sound oracle on each case, no input combination produces a failing result.

• Every condition combination of a bounded decision. A logic error that only some combination of conditions would expose, in eligibility, pricing, access, or control logic small enough to enumerate.

What it does not establish: the oracle half (the criterion proves every combination was run, never that each produced the right answer), and nothing beyond the bound (unbounded loops, real-typed inputs, or non-determinism collapse the corner).

When a coverage criterion becomes a proof

The corner needs three things at once; dropping any one collapses it back to a signal:

1. A finite, deterministic input space. The cases the code can take must be enumerable, and each case must behave the same way every time. Non-determinism (threads, clocks, external state) breaks this before anything else does.
2. An exhaustive criterion. Multiple-condition coverage (MCC) runs every combination of a decision's conditions: the full truth table. Over a finite space, running all of them is enumeration, and enumeration is a soundness proof (Zhu et al. 1997)¹: within those inputs, no failure exists.
3. A sound oracle. This is the half the coverage number cannot see. MCC guarantees every input combination was run; it says nothing about whether each run produced the right answer. Enumerating the truth table with no assertion proves only that nothing crashed. The proof is "no failure here" only if something checks each row for failure.

MC/DC is the engineering compromise on the exhaustive criterion. Full MCC is 2ⁿ in the conditions; MC/DC instead requires each condition be shown to independently flip the decision, which grows roughly linearly. It approximates the truth-table enumeration at tractable cost, which is exactly why safety-critical regimes mandate it rather than MCC (RTCA 2011; Hayhurst et al. 2001)^{2 3}. The approximation holds only inside the Boolean, deterministic envelope; it says nothing about the values flowing through a comparison, only about the branch.

Model checking is the same move made to scale. Predicate abstraction replaces a program's data with a finite set of Boolean predicates; reachability in the resulting Boolean program is decidable, so the checker settles it exhaustively (Ball et al. 2001)⁴: the abstraction chosen precisely so the finite case applies. A decision table over a small case space is the same idea by hand. All of these are stronger criteria than line or branch, and none is what a coverage tool reports by default.

When the space stops being finite

Add real types and unbounded flow and the corner disappears. The input combinations grow exponentially, and become unbounded once a loop ranges over input-controlled data, so enumerating them (MCC or path coverage) is intractable.

Tools

The method is measuring MC/DC or MCC over a decision, so the tools are coverage instruments that report those criteria, not just line and branch.

• Open source: mainstream toolchains now measure MC/DC directly: Clang's -fcoverage-mcdc (source-based coverage) and GCC's condition coverage (-fcondition-coverage, reported through gcov).
• Multiple-condition coverage: Testwell CTC++ is the rare tool that reports full MCC, the whole truth table, rather than the MC/DC approximation (commercial).
• Certification sign-off: the DO-178C-qualified avionics suites VectorCAST, LDRA, and Rapita measure MC/DC to the evidence standard a regulator accepts (commercial).

When to use, when not

Use:

• For bounded decision logic where every condition combination matters and the space is small enough to enumerate: eligibility, pricing, access, and safety-critical control logic.
• Where a regime mandates it. DO-178C requires MC/DC for the highest software levels, so the criterion is the certification evidence, not an optional extra.
• With a sound oracle on each case. Without one, the criterion proves reachability, not correctness, and the proof half is missing.

Don't:

• When the input space is unbounded or loop-driven over input-controlled data. Enumeration is intractable and line or branch coverage was never a proof to begin with; treat the number as a reachability signal and bound the domain or steer a search instead.
• When the code is non-deterministic. Threads, clocks, and external state break the finite-deterministic precondition before anything else does.
• As a percentage target. Raising an MC/DC number recovers nothing the enumeration did not already establish; the case against coverage as a goal is testing folklore.

Recovering a piece

Bound the domain explicitly. If the space is too large to exhaust, shrink it to one that can be, and say so. Bounded-exhaustive testing generates every structurally distinct input up to a stated size bound; Korat does this for linked data structures, deriving the inputs from their representation invariants (Boyapati et al. 2002)⁵. The justification is the small scope hypothesis: most faults are revealed by some small input, so exhausting the small cases catches them. MCC with a sound oracle is the same pattern on a decision-sized space, and is exactly what refinement and dependent types deliver by construction rather than by enumeration. It is not the random sampling property-based testing usually means, which works a large space and stays empirical (Lampropoulos et al. 2019)⁶; it is that method's enumeration sibling: the bounded-exhaustive instance of PBT, which exhausts a small space and earns a bounded proof. The guarantee is then exactly as wide as the declared bound.

Evidence

• Enumeration is a decision procedure, not a sample. Exercising every case of a finite space settles the bounded question outright, which is what lifts the strongest criteria from a reachability signal to a proof (Zhu et al. 1997)¹.
• The guarantee is the enumeration, not the percentage. With suite size held constant, coverage correlates only weakly with faults found (Inozemtseva and Holmes 2014)⁷; a high MC/DC number outside the finite, oracle-checked corner earns little.

Related

Exhaustive enumeration of a bounded input space, compressed several ways

These methods all exhaustively enumerate a bounded input space; each compresses the exponential blow-up a different way. Decision tables compress losslessly: a "don't-care" entry folds together combinations that share an outcome, so every case still maps to one rule, and the row carries its own expected decision. Combinatorial and pairwise testing sample: a covering array keeps every t-way interaction and drops the higher-order ones, with the oracle supplied separately. Bounded-exhaustive property testing bounds the size: it enumerates every value up to a depth/size k (SmallCheck), relying on the small-scope hypothesis that faults surface small. Exhaustive coverage runs from MCC (the full 2ⁿ truth table) down to MC/DC's n+1 independence criterion, and audits an existing suite rather than generating one. Type systems reach the same completeness by construction: an exhaustiveness check on a match / switch over a sum type has the compiler verify every variant is handled, with no case written by hand. State-, path-, and schedule-space enumerators such as model checking, symbolic execution, and systematic concurrency testing share the idea over a different space; see the reachability clusters.

Classification

• Quality dimensions: Functionality.
• Area: Bounded Boolean decision logic — eligibility / pricing / access rules, safety-critical control logic, anywhere a decision's condition combinations are few enough to enumerate.
• Guarantee: Exhaustive — MCC runs the full truth table, which over a finite deterministic space is a soundness proof; MC/DC is the tractable near-exhaustive substitute.

Referenced by

• Coverage · Methods
• Property-based testing · Methods
• Verifying safety-critical systems · Methods

References

---

1. Zhu, Hong, Patrick A. V. Hall, and John H. R. May. 1997. "Software Unit Test Coverage and Adequacy." ACM Computing Surveys 29 (4): 366–427. https://doi.org/10.1145/267580.267590. ↩↩

2. RTCA. 2011. DO-178C: Software Considerations in Airborne Systems and Equipment Certification. https://www.rtca.org/do-178/. ↩

3. Hayhurst, Kelly J., Dan S. Veerhusen, John J. Chilenski, and Leanna K. Rierson. 2001. A Practical Tutorial on Modified Condition/Decision Coverage. NASA/TM-2001-210876. https://ntrs.nasa.gov/citations/20010057789. ↩

4. Ball, Thomas, Rupak Majumdar, Todd Millstein, and Sriram K. Rajamani. 2001. "Automatic Predicate Abstraction of C Programs." Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation (PLDI '01), 203–13. https://doi.org/10.1145/378795.378846. ↩

5. Boyapati, Chandrasekhar, Sarfraz Khurshid, and Darko Marinov. 2002. "Korat: Automated Testing Based on Java Predicates." Proceedings of the 2002 ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA '02), 123–33. https://doi.org/10.1145/566172.566191. ↩

6. Lampropoulos, Leonidas, Michael Hicks, and Benjamin C. Pierce. 2019. "Coverage Guided, Property Based Testing." Proceedings of the ACM on Programming Languages 3 (OOPSLA): 181:1–29. https://doi.org/10.1145/3360607. ↩

7. Inozemtseva, Laura, and Reid Holmes. 2014. "Coverage Is Not Strongly Correlated with Test Suite Effectiveness." Proceedings of the 36th International Conference on Software Engineering (ICSE '14), 435–45. https://doi.org/10.1145/2568225.2568271. ↩