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's position is one value on each, or a set of oracle values where one run is judged by several oracles at once.

Guarantee (how strong a claim a passing run makes) 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 the reachable ceiling is rarely the tier a method actually achieves.

All of this classifies the method. Effect is a different kind of thing: a property of the code under test (what the code touches, from pure through stateful, I/O-bound and nondeterministic), 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. 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 and nothing else. A team running fuzzing only on pure functions and example tests on boundary-crossing code has gaps in the middle.

The argument about 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 levels 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 throws thousands of generated inputs at it, or a runtime assertion fires on the one that slips through in production. Contracts as specifications map this level-by-level.

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

The levels are a menu, not a hierarchy: the highest one the stakes justify is the one to use, and a lower one serves where the higher is infeasible — proof doesn't scale to a whole program, and unpredictable inputs surface only in production.

Locating methods on the axes

A few methods, picked to span the extremes of each axis:

Method Input Oracle Guarantee
Example test Fixed Any Empirical
Fuzzing Generative Errors 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.

Every method's full position, plus the quality dimensions it serves, is in the per-family tables in the methods catalog.

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. No study compares teams that use this framing with teams that use something else.

The model makes hidden decisions visible. A team using any single-axis taxonomy has implicitly chosen positions on the other axes (a fixed input, an equality oracle, and an empirical guarantee being the most common defaults) without acknowledging those are choices.

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, one per axis, into a single cross-method frame. 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; Lucassen and Gifford 1988)7 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 orthogonal frame spanning tests, types, formal methods, and monitoring (not the individual axes), used to tell look-alike methods apart — noting which single coordinate separates each confusable pair. 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. ↩