正确性判定器(Correctness Oracles)
选择一个能够反驳所承诺行为的可观察结果。明确一个成功检查留下什么未测试:计数比较、结构检查和依赖见证观察的是不同属性(NoREC 实现、SQLite 完整性检查、Elle §4.3)。
从实际边界推导检查
阅读目标系统的启用配置、公开生产者和约束合同。确定合法的起始状态、操作前提条件、允许的错误以及所承诺的边界:一次操作、语句、事务、恢复或观察到的历史。在 SQLite 中,ABORT 会撤销一条语句,而延迟外键“直到事务尝试 COMMIT 时才被检查”(SQLite ABORT,延迟外键)。尽可能查询生效的设置;例如,SQLite 的外键设置“在事务内无操作”(SQLite foreign_keys)。
在扩展搜索之前,先写一个具体的候选观察结果:
- 承诺: 确切的被禁止结果或效应,并附有合同引用。
- 观察: 实际返回的内容、状态或见证,用于区分该违规行为与允许行为。
- 前提条件和盲点: 支持的配置、有效状态、遗漏的信息和无法区分的执行。
- 重放证据: 输入和初始状态、操作序列、有效配置和原始观察结果。
这是一个紧凑的设计约定,而非必需的模板。其目的是暴露拟议检查所丢失的信息;Elle 的观察模型展示了为什么隐藏的依赖关系不能仅仅通过生成更多历史记录来恢复:盲写寄存器操作会“破坏历史”(Elle §§3–4.3)。阅读合约示例以了解已处理的边界。
在 JavaScript 中,进程退出码、测试运行器状态或干净的日志就是这样的观察结果:其含义取决于生效模式、已安装的监听器、运行器配置和构建。安装了 uncaughtException 处理器后,Node 的进程“将以 0 退出”,除非该处理器设置了 process.exitCode(Node 进程, uncaughtException)。阅读 JavaScript 观察渠道以了解 Node、测试运行器、React 和 Playwright 的渠道。
保持观察独立于被怀疑的行为
追溯期望值或不变量是如何获得的。识别可能让目标和检查器得出同一个错误答案的共享代码和假设。优先选择经过验证的抽象模型、独立指定的不变量或有效关系,而不是复制的生产算法。第二实现是一种选择:SQLite 的 SQL Logic Test 针对多个引擎运行语句,并检查“它们是否得到相同的答案”。同引擎关系是另一种选择:SQLite 禁用优化重新运行测试套件,SQLancer 的 NoREC 将优化查询与未优化查询进行比较(SQLite 测试 §2,§9,NoREC 实现)。
衡量实际比较的信息。相等的行数并不表明行标识相同;健康的 integrity_check 并不保证引用完整性,因为它“找不到外键错误”。保留有效的部分检查,并且仅当目标保证要求时才添加补充观察(NoREC 实现,SQLite 完整性检查)。在选择引用、规范化或见证时,阅读部分观察。
检查允许的错误及其效果
独立于返回的状态,推导出允许的后状态。SQLite 的 ABORT 和 FAIL 都返回约束错误,但 ABORT 会回滚失败的语句,而 FAIL “不回滚失败的 SQL 语句之前所做的更改”。仅基于错误的断言可能会遗漏错误的效果;粗暴的回滚断言可能会拒绝合法行为(SQLite 冲突策略)。
为实际承诺选择一个观察器,并确保有效的前提条件。对于 SQLite 引用检查,使用适用的外键观察结果、生效的执行设置和合法的 NULL 语义;不要用通用的完整性检查结果替代(SQLite 外键,foreign_key_check)。这些是已处理的合约,而非适用于任意 API 的默认值。
保留检查的结果和限制
每当这种差异影响结论时,区分已评估的属性与拒绝的输入、预期错误、跳过的检查和不充分的观察。NoREC 在任一方计数为 -1 哨兵值(例如,在预期查询错误之后)时跳过比较而不是将其计为相等,并将意外错误报告为失败。Elle 的完备性依赖于记录的信息,并且“观察很少是完备的”(NoREC 实现,Elle §4.3)。
使用 harness-sensitivity 来确定观察能够到达并拒绝对一个代表性和独立验证的违规行为。保留原始见证以便进行 evidence-based-triage:Elle 自身的文档建议“手动检查报告的反常情况”,而不是将标签视为最终权威(Elle README)。通用的搜索分配属于 bugfinding-campaign。
将所选的专业推理路由到 semantic-differential-testing, metamorphic-testing, linearizability-checking, transactional-history-testing, numerical-oracles, resource-complexity-testing 或 liveness-testing;本技能拥有合约到观察的决策权。阅读常见错误以了解误导性捷径。
返回可用的判定器
返回生产组件、引用的保证、有效的前提条件、可执行的观察结果和结果解释,并附带一个已处理的允许/禁止区分说明。说明哪些内容仍然不可观察,以及哪些证据必须在重放中保留。有见证的矛盾只支持实际检查的保证和假设(Elle §§4.3 和 9)。