Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.fuzzing

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

AHoF V11 Fuzzing: generate test inputs by repeatedly mutating a seed input and checking whether any mutant violates the specification. The primitive bit-flip mutation toggles a boolean coordinate of the input: flip b = if b then false else true (the not connective). Proved native and axiom-free: the flip mutation, and its involution law -- flipping twice restores the original bit (flip (flip b) = b) -- which is what lets a fuzzer explore and return: no mutation is unreachable or lost. The mutation-scheduling strategy and the coverage-guided seed selection are executable concerns; what is proved here is the mutation operator and its involution. Requires data/Bool and logic/if-data (both in the 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.fuzzing` prints this classification.

fuzzing/flip :
  (x₁ : data/Bool)
  → data/Bool

fuzzing/flip-true :
  → fuzzing/flip data/true = data/false

fuzzing/flip-false :
  → fuzzing/flip data/false = data/true

fuzzing/flip-involution-true :
  → fuzzing/flip (fuzzing/flip data/true) = data/true

fuzzing/flip-involution-false :
  → fuzzing/flip (fuzzing/flip data/false) = data/false