2. MC/DC定义与逻辑基础
MC/DC（Modified Condition/Decision Coverage，修正条件/判定覆盖）是航空机载软件结构覆盖测试中要求最高、也最能暴露逻辑缺陷的一类准则。它之所以被 DO-178C 列为 A 级软件的目标覆盖之一，是因为它同时约束了“判定结果是否被取到”和“每个条件是否被单独证明有影响”。要真正写出可执行的 MC/DC 用例，必须先厘清五个基础概念：条件、判定、条件组合、独立影响对、短路求值。
一、条件与判定：最小布尔单元与整体出口
条件（Condition）是指不能再分解为更小布尔表达式的原子布尔量。它通常来自一个关系表达式或一个布尔变量，例如 alt > 1000、gearDown、mode == AUTO。注意：alt > 1000 整体是一个条件，不能把 alt 和 1000 再拆成两个条件。
判定（Decision）是由一个或多个条件通过 &&、||、! 组合而成的布尔表达式，它决定程序的一个控制流向，例如 if (A && (B || C)) 中的 A && (B || C) 就是一个判定。判定是“整体”，条件是“成员”。一个判定可以只含一个条件（此时判定覆盖与条件覆盖重合），也可以含多个条件。
在机载软件中，判定往往对应一个安全关键分支，例如自动驾驶接通条件、起落架收放许可、告警触发逻辑。因此 MC/DC 的测试对象不是“某一行代码”，而是“某个判定及其内部条件结构”。
二、条件组合与真值表：把逻辑摊开
设判定 D = A && (B || C)，含 3 个条件。理论上 3 个条件共有 2³ = 8 种条件组合（真值组合）。把每种组合代入表达式，可得到对应的判定结果，这就是该判定的真值表。真值表是 MC/DC 用例设计的基础工具：它把“逻辑”变成“可枚举的行”。
需要强调的是，MC/DC 并不要求穷举全部 2ⁿ 行，而是要求对每个条件找到至少一对组合，使得“只有该条件不同、其余条件相同、判定结果不同”。这一对组合就是该条件的独立影响对（Independence Pair）。因此 MC/DC 的用例数通常介于“条件数 + 1”与“2×条件数”之间，远小于穷举。
三、独立影响对：MC/DC 的核心机制
对条件 X 而言，独立影响对是两行条件组合 (T1, T2)，满足：
- 在 T1 与 T2 中，除 X 外其余所有条件的取值完全相同；
- X 在 T1 与 T2 中取值相反；
- 判定 D 在 T1 与 T2 中结果相反。
这三点合起来说明：在“其他条件被固定住”的前提下，X 的翻转单独导致了判定翻转，即 X 对 D 具有独立影响。MC/DC 要求每个条件至少存在一个这样的独立影响对，并且这些对必须被实际测试用例覆盖。
以 D = A && (B || C) 为例，取 A=1、B=1 固定，令 C 从 0 变到 1：D 从 0 变到 1，得到 C 的独立影响对。取 A=1、C=0 固定，令 B 从 0 变到 1：D 从 0 变到 1，得到 B 的独立影响对。取 B=0、C=0 固定，令 A 从 0 变到 1：D 从 0 变到 1，得到 A 的独立影响对。三对组合即可覆盖全部条件，共 4 条用例（部分行可复用）。
四、短路求值：让“独立影响”变得微妙
在 C、C++、Ada 等语言中，&& 与 || 通常采用短路求值（Short-Circuit Evaluation）：A && B 中若 A 为假，则 B 不再求值；A || B 中若 A 为真，则 B 不再求值。这一语义对 MC/DC 有直接影响。
考虑 D = A && B。当 A=0 时，B 根本不会被求值，B 的“取值”在运行时并不存在。此时若想构造 B 的独立影响对，必须让 A=1，使 B 真正被求值，再令 B 从 0 变到 1，观察 D 从 0 变到 1。也就是说，短路求值会“屏蔽”某些条件，使部分真值表行在运行时不可达。测试用例设计时必须区分“逻辑真值表行”与“运行时实际可达行”。
更隐蔽的是带副作用的表达式，例如 if (readSensor() && flag)。短路会导致 readSensor() 在某些用例中不被调用，从而影响硬件状态、计数器或时序。MC/DC 用例不仅要覆盖条件取值，还要保证被屏蔽的调用不会破坏其他用例的前置状态。工程上常见的做法是：把带副作用的函数调用从判定中移出，先求值到临时变量，再参与判定，使条件成为纯布尔量，降低 MC/DC 用例之间的耦合。
五、形式化定义与判定结构
把上述概念形式化：设判定 D 含条件集合 C = {c₁, c₂, …, cₙ}，每个条件取值于 {0,1}。一个测试用例对应一个赋值向量 v ∈ {0,1}ⁿ，D(v) 为判定结果。MC/DC 覆盖要求：对每个 cᵢ，存在两个可达赋值向量 v₁、v₂，使得：
- v₁ 与 v₂ 仅在 cᵢ 上不同；
- D(v₁) ≠ D(v₂)。
若判定中还存在“多条件耦合”，例如 (A && B) || (C && D)，则某些条件可能不存在独立影响对（例如 A 与 B 完全对称时，单独翻转 A 可能无法改变结果）。此时需要借助等价类划分或改写判定结构，使每个条件都能被独立证明。这也是为什么在安全关键软件中，评审常建议把复杂判定拆成多个简单判定，或引入中间布尔变量，以降低 MC/DC 用例设计难度并提高可分析性。
六、一个可操作的 MC/DC 用例设计流程
- 从代码或模型中提取判定 D，列出全部原子条件 c₁…cₙ，确认没有把关系表达式误拆。
- 按目标语言语义确定短路规则，标出哪些条件组合在运行时不可达。
- 对每个条件 cᵢ，固定其余条件，寻找使 D 翻转的取值对，形成独立影响对。
- 合并可复用的赋值向量，得到最小或接近最小的用例集合。
- 为每条用例填写输入、预期判定结果、实际判定结果与覆盖的条件，形成可追溯记录。
以 D = A && (B || C) 为例，一组满足 MC/DC 的用例可设计为：(A,B,C) = (1,0,0) → D=0；(1,0,1) → D=1；(1,1,0) → D=1；(0,0,0) → D=0。其中 (1,0,0) 与 (1,0,1) 构成 C 的独立影响对，(1,0,0) 与 (1,1,0) 构成 B 的独立影响对，(1,0,0) 与 (0,0,0) 构成 A 的独立影响对。四条用例覆盖三个条件，且每条都对应真实可执行的输入组合。