CsCheck
Use CsCheck to explore inputs and action sequences; keep the application's contract visible in the test. Let the library generate, shrink, print, and replay counterexamples. Start with the smallest test that can falsify the claim, rather than building a testing framework around CsCheck.
Choose the test shape
| What needs checking | Start with | Read when needed |
|---|---|---|
| A function, round trip, algebraic law, or data transformation | Gen + Sample | Properties and generators |
| An implementation with a simpler reference representation | SampleModelBased / SampleModelBasedAsync | Stateful and async tests |
| A protocol or lifecycle with explicit state, guards, and requirements | Spec.From, then Exhaustive and Conform | Executable specifications |
| Async resources or expectations that must incorporate observed outcomes | Generated command arrays + SampleAsync, with cleanup inside each case | Stateful and async tests |
| A failing property, seed replay, or a before/after bug demonstration | Native sampling controls and a concrete regression | Failure discovery and replay |
Read only the references needed for the task. These examples use xUnit, but CsCheck itself is test-framework independent. Preserve the project's existing framework and package-management conventions.
Establish the contract first
Identify an observable requirement and a plausible wrong result it would reject. Separate generated inputs, expected behavior, and actual observations. A model may consume observations, but must validate them against prior expectations before accepting them as new state. Do not use the implementation's answer to manufacture its expected answer.
Generate individual operations and their arguments, allowing CsCheck to compose arbitrary sequences. Finite domains, weighted boundary values, and preconditions are legitimate modeling choices. Handwritten whole scenarios are useful regressions, but are not a substitute for exploring action orderings.
Keep rejected requests testable when rejection is part of the contract. A guard saying “only withdraw when funds exist” cannot test insufficient-funds rejection. Preconditions describe what can be attempted; postconditions describe the response, including allowed failures.
Keep the test machinery small
- Prefer composed
Genvalues toRandom, hand-chosen seed lists, custom shrinkers, or retries-until-green. - Construct a fresh mutable implementation and model for each generated case, including shrinking.
- Use ordinary records, direct calls, and meaningful comparisons.
equal:must compare behavior or state; cleanup belongs infinally/using, not an equality predicate that always returns true. - Keep seeds out of ordinary discovery runs. Replay a seed emitted by a failure, then pin concrete inputs when the regression must survive generator changes.
- Preserve domain coverage and historical counterexamples when simplifying. Fewer lines alone do not establish that the replacement checks the same behavior.
Verify the right thing
Spec.Exhaustive checks the model. Spec.Conform checks the real implementation through the adapter
and only for sampled traces and compared observations. Keep both claims explicit. Inspect unreachable
requirements, deadlocks, and search cutoffs; a green run can be vacuous.
When practical, show that the test rejects a known broken implementation or a small deliberate defect in an isolated copy. Compile and execute examples rather than assuming similarly named FsCheck APIs exist in CsCheck. Reuse native model-based APIs when their independent transitions and comparison fit; a custom async loop is a useful alternative, not a universal replacement.
API baseline
The linked examples were compiled and run with CsCheck 4.9.1 on .NET 8. Its package identifies
source revision 5050355.
Check the installed package before adapting signatures. For upgrades, verify the
NuGet package and upstream source; do not infer a major version
or native async Spec.Conform support from another library's API.
