Module Windtrap_prop.PropSource

Property runner and configuration.

Property-based testing runner.

This module provides the core property checking logic. It generates random inputs, tests properties, and shrinks failing cases to find minimal counterexamples.

Sourceexception Reject

Raised to discard the current test case. Prefer assume or reject instead of raising directly.

Sourceval assume : bool -> unit

assume b discards the current test case if b is false. Prefer constrained generators when possible, as excessive discarding causes the test to return result.Gave_up.

Sourceval reject : unit -> 'a

reject () unconditionally discards the current test case.

Sourceval collect : string -> unit

collect label records label for the current generated case.

Collected labels are reported as a distribution. A label is counted at most once per generated case, even if collect is called multiple times.

Sourceval classify : string -> bool -> unit

classify label cond is if cond then collect label.

Sourceval cover : label:string -> at_least:float -> bool -> unit

cover ~label ~at_least cond declares a coverage requirement and records a hit for label when cond is true.

Coverage is checked over successful (non-discarded) cases. The property fails with result.Coverage_failed when label appears in less than at_least percent of successful cases.

  • raises Invalid_argument

    if at_least is not in [0.0, 100.0], or if the same label is used with conflicting thresholds in one property run.

Configuration

Sourcetype config = {
  1. count : int;
    (*

    Number of successful tests required. Default: 100.

    *)
  2. max_gen : int;
    (*

    Maximum generation attempts (including discards). Default: 300.

    *)
  3. max_shrink : int;
    (*

    Maximum shrink steps. Default: 100.

    *)
  4. seed : int option;
    (*

    Random seed. None reads the WINDTRAP_SEED environment variable, falling back to a random seed.

    *)
}

Property test configuration.

Sourceval default_config : config

Default configuration: 100 tests, 300 max gen, 100 max shrink, no fixed seed.

Sourceval set_default_seed : int option -> unit

set_default_seed seed sets a global default seed used when config.seed is None and WINDTRAP_SEED is not set. Called by Windtrap.run to propagate the CLI --seed flag to property tests.

Sourceval set_default_count : int option -> unit

set_default_count count sets a global default test count used when no explicit config.count override is provided. Called by Windtrap.run to propagate the CLI --prop-count flag.

Results

Sourcetype coverage_issue = {
  1. label : string;
  2. required : float;
  3. actual : float;
  4. hits : int;
}

A coverage requirement that was not met.

Sourcetype result =
  1. | Success of {
    1. count : int;
    2. discarded : int;
    }
    (*

    Property passed for count inputs, discarding discarded cases.

    *)
  2. | Failed of {
    1. count : int;
    2. discarded : int;
    3. seed : int;
    4. counterexample : string;
    5. shrunk_counterexample : string;
    6. shrink_steps : int;
    }
    (*

    Property failed. Shows original and shrunk counterexamples.

    *)
  3. | Error of {
    1. count : int;
    2. seed : int;
    3. counterexample : string;
    4. exn : exn;
    5. backtrace : string;
    }
    (*

    Property raised an unexpected exception.

    *)
  4. | Coverage_failed of {
    1. count : int;
    2. discarded : int;
    3. seed : int;
    4. missing : coverage_issue list;
    5. collected : (string * int) list;
    }
    (*

    Property predicate passed, but one or more coverage requirements were not met.

    *)
  5. | Gave_up of {
    1. count : int;
    2. discarded : int;
    3. seed : int;
    }
    (*

    Generation attempts reached max_gen before count tests passed.

    *)

Result of running a property test.

Running Properties

Sourceval check : ?config:config -> ?rand:Random.State.t -> 'a Arbitrary.t -> ('a -> bool) -> result

check arb prop tests that prop holds for all values from arb.

On failure, attempts to shrink the counterexample to find a minimal failing case. Returns detailed result with counterexample and shrink info.

  • parameter config

    Test configuration. Uses default_config if not provided.

  • parameter rand

    Random state. If not provided, derives from config seed or environment.