Coverage is not correctness: tests still need expected results

Q: Does MC/DC coverage guarantee catching it?

MC/DC on the intended rule requires a row pair that shows banned matters, and one of those rows is a banned member, so yes for this slip. It is still coverage of the intended rule's structure, not a proof of correctness in general.

A test suite can cover every input and every branch of a rule and still miss the bug, because coverage measures what the tests touched, not whether the expected results were right. The two formulas below differ on two rows, and a suite can cover both formulas fully without visiting either.

The intended rule is (member OR invited) AND NOT banned; the buggy one is member OR (invited AND NOT banned), the grouping slip. They differ on the rows member = TRUE, invited = FALSE, banned = TRUE and member = TRUE, invited = TRUE, banned = TRUE: the buggy rule admits banned members. The equivalence check reports the first of these as the counterexample. Every other row agrees, six of eight.

Now consider a suite of four tests: a plain member, an invited non-member, a stranger, and an invited person who is banned. It exercises every input in both values, both outcomes, and every branch of the buggy formula, so every coverage measure reads one hundred percent. It never tries a banned member, so it passes on the buggy rule. The coverage was real; the oracle was incomplete.

Coverage tells you which rows your tests reached. Correctness needs the expected result for each row to come from the requirement, not from running the code, and it needs the rows where a mistake would show, which is what independence pairs and counterexamples give you. The testing section has the full workflow; the step in the lesson on test design puts it in one sentence: expected results come from the requirement.

intended := (member OR invited) AND NOT banned · outputbuggy := member OR (invited AND NOT banned) · output

Are intended and buggy equivalent? No Counterexample: member = T, invited = F, banned = T · Exhaustively checked and solver cross-checked · 6 rows

Truth table

They differ on this row: #5, #7

Coverage is not correctness: tests still need expected results
#	member	invited	banned	intended	buggy
0	FALSE	FALSE	FALSE	FALSE	FALSE
1	FALSE	FALSE	TRUE	FALSE	FALSE
2	FALSE	TRUE	FALSE	TRUE	TRUE
3	FALSE	TRUE	TRUE	FALSE	FALSE
4	TRUE	FALSE	FALSE	TRUE	TRUE
5	TRUE	FALSE	TRUE	FALSE	TRUE
6	TRUE	TRUE	FALSE	TRUE	TRUE
7	TRUE	TRUE	TRUE	FALSE	TRUE

Plain-language reading

Beginnerintended is true exactly when both of the following hold:
1. at least one of member or invited is true (both may be true)
2. banned is false
In every other case, intended is false.
About the operators:
- AND is true only when all of its parts are true.
- OR is inclusive: it is true when at least one part is true, including when several are.
- NOT reverses a value: true becomes false and false becomes true.

Intermediateintended is true exactly when both of the following hold:
1. at least one of member or invited is true (both may be true)
2. banned is false
In every other case, intended is false.

Advancedintended is true exactly when both of the following hold [conjunction ∧]:
1. at least one of member or invited is true (both may be true) [inclusive disjunction ∨]
2. banned is false [negation ¬]
In every other case, intended is false.
Formal notation: (member ∨ invited) ∧ ¬banned

The common slip

Reporting a coverage figure as evidence that a rule is right. The figure says the tests ran the code; it says nothing about whether anyone checked the answers against the requirement, and the two rows that expose this bug can be absent from a fully covering suite.

Questions

What would have caught this bug?

A test for a banned member, which is the counterexample the equivalence check replays, and more generally an independence pair for banned: two rows that differ only in that input and give different results under the intended rule.

Does MC/DC coverage guarantee catching it?

MC/DC on the intended rule requires a row pair that shows banned matters, and one of those rows is a banned member, so yes for this slip. It is still coverage of the intended rule's structure, not a proof of correctness in general.

Worked examples

Entry rule slip: member OR (invited AND NOT banned) and the case that differs

Tools

Pitfalls

Generated from the Tangibool engine, semantics tangibool-semantics/1, engine 1.0.0, build 2026-11-07. Every table, map, simplification and verdict on these pages was computed by the Tangibool engine when the site was built, and every claim was re-checked by the same exact checker the app uses. Limits are stated where they apply. © 2026 Foreranger LTD.