data Trace = MkTrace (List String) (List String) (Maybe Int) -- inputs, labels, trials askedCe qu'une exécution accumule : les entrées forAll rendues (pour le rapport d'échec) et les étiquettes statistiques (pour le résumé de distribution).
importPour l'utiliser :
import Data.TestData.Test — la monade Property (tests par propriétés en style do)
Synopsis
data Trace = MkTrace (List String) (List String) (Maybe Int) -- inputs, labels, trials askeddata Outcome adata Property a = MkProp (Gen (Pair Trace (Outcome a)))forAll : Show a => Gen a -> Property awithTests : Int -> Property ()(===) : Eq a => Show a => a -> a -> Property ()(/==) : Eq a => Show a => a -> a -> Property ()assert : Bool -> Property ()claimHolds : String -> a -> a -> Property ()claimInput : Gen a -> Property asameSet : Ord a => Eq a => Show a => List a -> List a -> Property ()withinAbs : Double -> Double -> Double -> Property ()withinRel : Double -> Double -> Double -> Property ()satisfies : Show a => a -> (a -> Bool) -> Property ()classify : String -> Bool -> Property ()label : String -> Property ()collect : Show a => a -> Property ()data CheckResult =data Check =checkStart : CheckcheckStep : Int -> Int -> Int -> Property a -> Check -> CheckcheckProperty : Int -> Int -> Int -> Property a -> CheckResult
data Outcome a
= Done a
| Failed StringLe résultat des assertions d'une propriété : une valeur, ou le premier échec.
Donel'essai a terminé avec une valeur
Failedune assertion a échoué, avec son message
data Property a = MkProp (Gen (Pair Trace (Outcome a)))Property a = Gen (Trace, Outcome a) : un générateur (portant l'arbre de rétrécissement) d'une issue tracée.
forAll : Show a => Gen a -> Property aTire une valeur d'un générateur, en l'enregistrant (via show) pour le rapport d'échec. L'arbre de rétrécissement du générateur devient celui de la propriété : en cas d'échec, la valeur tirée rétrécit vers l'origine de son générateur.
withTests : Int -> Property ()Ask for n trials of this property, whatever the suite's default (oppi test --tests, [test] property_tests, or the pinned 100). A statement anywhere in the block; the last one written wins. n must be at least 1: a property is checked by running it.
(===) : Eq a => Show a => a -> a -> Property ()Affirme l'égalité de deux valeurs ; en cas d'échec le rapport montre les deux côtés.
(/==) : Eq a => Show a => a -> a -> Property ()assert : Bool -> Property ()Affirme qu'un booléen tient.
claimHolds : String -> a -> a -> Property ()Judge the claim x ≡ y of a specification (conn: the connector as written, quoted when the two sides cannot be compared). On failure the report shows both sides, printed by the runner.
claimInput : Gen a -> Property asameSet : Ord a => Eq a => Show a => List a -> List a -> Property ()Égales à permutation près : mêmes éléments, mêmes multiplicités, ordre ignoré. À utiliser quand l'ordre du résultat n'est pas spécifié (p. ex. l'ensemble des couleurs / sommets d'un graphe).
withinAbs : Double -> Double -> Double -> Property ()Égales à une tolérance ABSOLUE ε près : |a - b| ≤ ε.
withinRel : Double -> Double -> Double -> Property ()Égales à une tolérance RELATIVE p de la référence : |a - b| ≤ p·|b| (withinRel 0.01 signifie « à 1 % près »).
satisfies : Show a => a -> (a -> Bool) -> Property ()La valeur satisfait un prédicat (pour les specs sans réponse unique). Se lit bien en infixe : result satisfies isSorted.
classify : String -> Bool -> Property ()Étiquette cette exécution avec lbl quand cond tient — le résumé rapporte le % d'exécutions ainsi étiquetées (pour voir la distribution produite par vos générateurs).
label : String -> Property ()Étiquette toujours cette exécution avec lbl.
collect : Show a => a -> Property ()Étiquette cette exécution avec show x — collecte une distribution de valeurs.
data CheckResult =
Passed Int (List (Pair String Int))
| Falsified Int (List String) String (List (Pair String Int))L'issue de la vérification d'une propriété numTests fois.
Passedtous les essais ont réussi : essais menés, décompte des étiquettes
Falsifiedun contre-exemple : numéro d'essai, entrées rétrécies, message, décompte
data Check =
Running Int (List (Pair String Int)) (Maybe Int)
| Finished CheckResultThe state of a check between two trials: how many trials have passed, the label tally so far, and the number of trials the property asked for (Nothing until a trial says, via withTests) — or the final result.
Runningtrials passed so far, label tally, trials asked
Finishedthe check is over
checkStart : CheckWhere every check starts.
checkStep : Int -> Int -> Int -> Property a -> Check -> CheckONE trial of prop — the single authority for what a trial is: draw the inputs at size from the seed of trial t (mixed from base), run the assertions, tally the labels, and on the first falsifying trial shrink it to a minimal failing input. checkProperty below is nothing but the iteration of this step; the test runner (oppi test, the browser engine) iterates the SAME step from outside, one evaluation per trial, so the evaluator's divergence guard (step and time budgets) applies PER TRIAL: a trial that loops costs one budget, never the budget of all the trials.
numTests is the SUITE's count (the runner's cascade); a property that asks for its own (withTests) is heard from its first trial on, and its count replaces the suite's for the rest of the check.
checkProperty : Int -> Int -> Int -> Property a -> CheckResultExécute prop jusqu'à numTests fois à la taille size, semée déterministiquement depuis base. Au premier essai falsifiant, le rétrécit vers une entrée minimale qui échoue et s'arrête ; sinon rapporte la distribution des étiquettes.