Skip to content

Software Quality

The axes

The project classifies every verification method by where its inputs come from and how its output is judged. Two more axes complete the frame: the guarantee a passing run earns and the effect scope a method reaches. Each method page carries its own Classification section.

Input and oracle are independent: a method takes one input value, or none for a static method, and one oracle value or a set of them where one run is judged by several oracles at once.

Guarantee is not a third independent axis: it is capped by the other two and derived from them (why). It is still recorded per method, because a method can sit below the ceiling its input and oracle allow.

All of this classifies the method. Effect is a different kind of thing: a property of the code under test (what the code touches: state, I/O and nondeterminism), read to select an adequate method. From the method's side the same cut becomes effect scope, and that is what a method page records.

The terminology page maps the conventional test categories onto the axes.

What the model is for

Methods become comparable on a shared axis. "Should we add property tests or fuzzing?" is a question about input and oracle. Both apply to pure functions; the difference is whether the inputs are schema-shaped or unfiltered, and what oracle each carries.

A suite's own gaps become visible. A team running only example tests has covered one column of the input axis. A team running fuzzing only on pure functions and example tests on boundary-crossing code has a gap between them: code with state that crosses no boundary gets neither.

The argument about test levels dissolves. Most of the energy spent on "what level is this test?" belongs instead in "where do the inputs come from, and what's the oracle?" The axes give specific names to the decisions the test-level vocabulary hides.

The same check at three rigor levels

Methods that look unrelated are often one question asked at different strengths. Where the oracle stays fixed — what gets checked — and only the input varies, a single property splits across families under separate names. How much of the input space a run covers sets the guarantee: a property can be proved for all inputs, tested on a sample, or observed on live traffic.

One such property is the predicate x > 0:

Level Method Family
Proved (all inputs) refinement & dependent types, theorem proving types / formal
Tested (sampled inputs) property-based testing tests
Observed (live inputs) contracts & runtime assertions runtime

The same predicate is checked three ways: a type system rejects the program for it, a property test runs thousands of generated inputs against it, or a runtime assertion fires on the one that slips through in production. Contracts as specifications tables the systems that attach such a predicate to code by how each discharges it.

The pattern isn't special to that oracle. Equivalence between a new implementation and the old one splits the same way:

Level Method Family
Proved (all inputs) equivalence checking formal
Tested (sampled inputs) differential testing tests
Observed (live inputs) parallel run runtime

Proof is the strongest level. Testing and observation both earn an empirical guarantee and differ in where their inputs come from, not in strength. The stakes decide whether a check has to reach proof, which is expensive at whole-program scale, and unpredictable inputs surface only in production.

Locating methods on the axes

A few methods, picked to span the extremes of the input, oracle and guarantee axes:

Method Input Oracle Guarantee
Example test Fixed Any Empirical
Fuzzing Generative Errors + predicate Empirical
Type checking — Predicate (type) Exhaustive¹
seL4-style proof — Predicate Mathematical
Production monitoring Live Probabilistic Heuristic

¹ Within the explicit bounds of what the type system is able to express.

The per-family tables in the methods catalog give every method's input, oracle and guarantee, plus the quality dimensions it serves.

Visibility (black-box, gray-box, white-box) is not one of the axes: a method keeps its coordinates whether or not the source is at hand. It decides which coordinates are available — a generative-feedback input needs a feedback channel, and a structural coverage criterion needs instrumentation. The terminology page sets out the gradient.

The model is a device, not a claim

The axes claim no empirical superiority over any other vocabulary.

A team using any single-axis taxonomy has implicitly chosen positions on the other axes without acknowledging those are choices, commonly a fixed input, an equality oracle, and an empirical guarantee.

The model is for thinking, not for ranking. The ranking question (which methods actually catch bugs?) is the empirical question answered case by case in the methods catalog.

Prior taxonomies

The axes are not new: they assemble established taxonomies. Where the field already has a standard vocabulary, the axes reuse it:

  • Oracle ← Barr et al.'s oracle survey (Barr et al. 2015)1: specified / derived / implicit / human, refined by metamorphic arity (Chen et al. 2018)2 and the atomic-vs-aggregated cut (Dobslaw et al. 2025)3.
  • Input ← Anand et al.'s test-generation survey (Anand et al. 2013)4: random, search-based, symbolic, combinatorial, model-based.
  • Guarantee ← soundness (program analysis) for the tiers; assurance levels (RTCA 2011; IEC 2006)5 6 are a related but distinct scale (consequence of failure, not claim strength), not the tiers' source.
  • Effect ← Koka's effect rows (Leijen 2014)7, rooted in the original effect calculus (Lucassen and Gifford 1988)8, and Google's test size (Winters et al. 2020)9, recomposed for testing (chiefly by splitting nondeterminism into magnitude tiers).

What's specific here is the assembly: one frame spanning tests, types, formal methods, and monitoring, used to tell look-alike methods apart. A 2025 faceted taxonomy for LLM testing organizes around SUT / Goal / Oracle / Input (Dobslaw et al. 2025)3; the faceting approach recurs, though that work shares an author with the oracle survey and its facets don't map one-to-one to ours, so it is lineage, not independent confirmation.

Referenced by

References

  1. Barr, Earl T., Mark Harman, Phil McMinn, Muzammil Shahbaz, and Shin Yoo. 2015. "The Oracle Problem in Software Testing: A Survey." IEEE Transactions on Software Engineering 41 (5): 507–25. https://doi.org/10.1109/TSE.2014.2372785. ↩

  2. Chen, Tsong Yueh, Fei-Ching Kuo, Huai Liu, et al. 2018. "Metamorphic Testing: A Review of Challenges and Opportunities." ACM Computing Surveys 51 (1): 1–27. https://doi.org/10.1145/3143561. ↩

  3. Dobslaw, Felix, Robert Feldt, Juyeon Yoon, and Shin Yoo. 2025. Challenges in Testing Large Language Model Based Software: A Faceted Taxonomy. arXiv:2503.00481. https://doi.org/10.48550/arXiv.2503.00481. ↩↩

  4. Anand, Saswat, Edmund K. Burke, Tsong Yueh Chen, et al. 2013. "An Orchestrated Survey of Methodologies for Automated Software Test Case Generation." Journal of Systems and Software 86 (8): 1978–2001. https://doi.org/10.1016/j.jss.2013.02.061. ↩

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

  6. IEC. 2006. IEC 62304: Medical Device Software — Software Life Cycle Processes. https://webstore.iec.ch/en/publication/6792. ↩

  7. Leijen, Daan. 2014. "Koka: Programming with Row Polymorphic Effect Types." Proceedings of MSFP 2014 (Mathematically Structured Functional Programming) 153: 100–126. https://doi.org/10.4204/EPTCS.153.8. ↩

  8. Lucassen, John M., and David K. Gifford. 1988. "Polymorphic Effect Systems." Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '88), 47–57. https://doi.org/10.1145/73560.73564. ↩

  9. Winters, Titus, Tom Manshreck, and Hyrum Wright, eds. 2020. Software Engineering at Google: Lessons Learned from Programming Over Time. O'Reilly Media. https://abseil.io/resources/swe-book/html/ch11.html. ↩