# Exhaustive coverage (MC/DC, MCC) 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](https://quality.stereobooster.com/coverage.md) 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](https://quality.stereobooster.com/decision-tables.md) 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)[^zhu1997]: 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](https://quality.stereobooster.com/coverage.md) 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)[^do178c] [^hayhurst2001]. 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](https://quality.stereobooster.com/model-checking.md) 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)[^ball2001]: the abstraction chosen precisely so the finite case applies. A [decision table](https://quality.stereobooster.com/decision-tables.md) 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](https://gcc.gnu.org/onlinedocs/gcc/Gcov.html)). - **Multiple-condition coverage:** [Testwell CTC++](https://www.verifysoft.com/en_ctcpp.html) 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](https://quality.stereobooster.com/testing-folklore.md). ## 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](https://korat.sourceforge.net/) does this for linked data structures, deriving the inputs from their representation invariants (Boyapati et al. 2002)[^boyapati2002]. 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](https://quality.stereobooster.com/refinement-and-dependent-types.md) 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)[^lampropoulos2019]; it is that method's enumeration sibling: the [bounded-exhaustive instance](https://quality.stereobooster.com/property-based-testing.md) 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)[^zhu1997]. - **The guarantee is the enumeration, not the percentage.** With suite size held constant, coverage correlates only weakly with faults found (Inozemtseva and Holmes 2014)[^inozemtseva2014]; 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](https://quality.stereobooster.com/decision-tables.md) 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](https://quality.stereobooster.com/combinatorial-testing.md) *sample*: a covering array keeps every *t*-way interaction and drops the higher-order ones, with the oracle supplied separately. [Bounded-exhaustive property testing](https://quality.stereobooster.com/property-based-testing.md) *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](https://quality.stereobooster.com/coverage.md) · Methods - [Property-based testing](https://quality.stereobooster.com/property-based-testing.md) · Methods - [Verifying safety-critical systems](https://quality.stereobooster.com/safety.md) · Methods ## References [^zhu1997]: Zhu, Hong, Patrick A. V. Hall, and John H. R. May. 1997. "[Software Unit Test Coverage and Adequacy](https://www.cs.toronto.edu/~chechik/courses18/csc410/p366-zhu.pdf)." *ACM Computing Surveys* 29 (4): 366–427. . [^do178c]: RTCA. 2011. *[DO-178C: Software Considerations in Airborne Systems and Equipment Certification](https://www.rtca.org/do-178/)*. . [^hayhurst2001]: Hayhurst, Kelly J., Dan S. Veerhusen, John J. Chilenski, and Leanna K. Rierson. 2001. *[A Practical Tutorial on Modified Condition/Decision Coverage](https://ntrs.nasa.gov/citations/20010057789)*. NASA/TM-2001-210876. . [^ball2001]: Ball, Thomas, Rupak Majumdar, Todd Millstein, and Sriram K. Rajamani. 2001. "[Automatic Predicate Abstraction of C Programs](https://web.cs.ucla.edu/~todd/research/pldi01.pdf)." *Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation (PLDI '01)*, 203–13. . [^boyapati2002]: Boyapati, Chandrasekhar, Sarfraz Khurshid, and Darko Marinov. 2002. "[Korat: Automated Testing Based on Java Predicates](https://mir.cs.illinois.edu/~marinov/publications/BoyapatiETAL02Korat.pdf)." *Proceedings of the 2002 ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA '02)*, 123–33. . [^lampropoulos2019]: Lampropoulos, Leonidas, Michael Hicks, and Benjamin C. Pierce. 2019. "[Coverage Guided, Property Based Testing](https://lemonidas.github.io/pdf/FuzzChick.pdf)." *Proceedings of the ACM on Programming Languages* 3 (OOPSLA): 181:1–29. . [^inozemtseva2014]: Inozemtseva, Laura, and Reid Holmes. 2014. "[Coverage Is Not Strongly Correlated with Test Suite Effectiveness](https://www.cs.ubc.ca/~rtholmes/papers/icse_2014_inozemtseva.pdf)." *Proceedings of the 36th International Conference on Software Engineering (ICSE '14)*, 435–45. . ## Acronyms - MC/DC — modified condition/decision coverage - MCC — multiple-condition coverage - PBT — property-based testing