Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.mutation-testing

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/mutation_testing.clj2 definitions, 4 theorems

AHoF V-family Mutation Testing: assess a test suite's fault-detection power by seeding many small program mutants and measuring how many the suite KILLS (detects). The mutation score is the exact rational fraction of killed mutants, and the suite is adequate when it meets a target threshold: mutation-score killed total = killed / total adequate? score threshold = decide (threshold <= score) over exact rationals. Proved native and axiom-free: the score formula; a worked score; the adequacy decision; the certificate that an adequate suite really meets the threshold (threshold <= score as native nnrat/at-most); and that a suite below the target is inadequate. The mutant generation and the test runs are executable; what is proved is the mutation-score and adequacy decision. Requires nnrat/divide (rational-division capability, composed here), audit/decide-nnrat-at-most, nnrat/at-most, nnrat/decide-at-most-true-sound (D63 checkpoint). Scope (measured by the kernel): this module has 4 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.mutation-testing` prints this classification.

Depends onmath.rational.division

mutation/score :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

mutation/adequate? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

mutation/score-example :
  → mutation/score 3 4 = 3/4

mutation/adequate-when-above :
  → bo/is-safe 3/4 1/2 = data/true

mutation/adequate-meets-threshold :
  → 1/2 ≤ 3/4

mutation/inadequate-when-below :
  → bo/is-safe 1/4 1/2 = data/false