Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.falsification

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

AHoF V9 Direct Sampling Falsification: the simplest falsification method -- sample inputs, simulate, and return the first whose specification robustness has dropped to the falsification margin. An input falsifies the specification when its robustness margin is at most the threshold: falsifies? robustness margin = decide (robustness <= margin) over the decidable rational order (robustness measured as a nonnegative margin above violation; margin 0 is exact violation). Defined: the falsification test. Proved native and axiom-free, as worked instances: robustness 1 with margin 2 is flagged, robustness 5 with margin 2 is not, and the worked certificate 1 <= 2 (native nnrat/at-most). Soundness of the test for all inputs (every reported counterexample is genuine) is not proved here. The input sampling and the simulation that produces the robustness value are executable. Requires nnrat/at-most, audit/decide-nnrat-at-most, and nnrat/decide-at-most-true-sound (all in the D63 checkpoint). Scope (measured by the kernel): this module has 3 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.falsification` prints this classification.

falsification/falsifies? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

falsification/flags-counterexample :
  → ce-is/elite? 1 2 = data/true

falsification/counterexample-is-sound :
  → 1 ≤ 2

falsification/robust-not-flagged :
  → ce-is/elite? 5 2 = data/false