Property-based testing in C#: invariants that find bugs

The bill-splitting helper passes its tests. A hundred cents divided between two people produces fifty cents each. Three hundred cents divided between three people produces a hundred each. Then someone splits a hundred cents between three people and one cent disappears. Every example in the suite used an amount divisible by the number of people. The implementation silently depended on a pattern nobody intended to promise.

Property-based testing starts with the promise instead of the examples. For every valid bill and group size, the allocated amounts must add up to the original bill. A test runner generates inputs, checks that statement, and reduces a failing input into a smaller explanation. You still write assertions. You stop being the only person choosing the numbers that reach them.

An invariant is a statement that must remain true across a defined input domain. For this helper, the domain is a nonnegative amount in whole cents and a positive number of recipients. We avoid currency conversion and fractional cents deliberately. Those belong to different contracts.

The result has four obligations: return one share per recipient, preserve the total, never create a negative share, and keep the largest and smallest shares at most one cent apart. Equal splitting cannot always produce identical shares, but it can preserve money while distributing the remainder.

A useful property says what every answer must preserve, including answers you would never have thought to put in a test case.

The invariant is stronger than "the result looks reasonable" and cheaper to specify than a table of every valid input. It also exposes a requirements question: who gets the leftover cent? Our contract assigns remainder cents to the earliest recipients. The general properties above do not prove that ordering rule, so we will keep a specific example for it.

These examples use FsCheck 3.4.0 with an existing xUnit v2 test project. The FsCheck.Xunit package targets that runner; xUnit v3 projects use the separate FsCheck.Xunit.v3 package. Pin the integration appropriate to your project rather than mixing runner generations.

dotnet add package FsCheck.Xunit --version 3.4.0
dotnet test

Here is the original bug, isolated into a small function. Returning an array makes the result easy to observe without relying on a database, a service container, or an application host.

public static class BillSplitter
{
    public static int[] Split(int cents, int people)
    {
        ArgumentOutOfRangeException.ThrowIfNegative(cents);
        ArgumentOutOfRangeException.ThrowIfNegativeOrZero(people);

        return Enumerable.Repeat(cents / people, people).ToArray();
    }
}

Use a domain type so that the generator describes one coherent case. Gen.Choose includes both endpoints. This generator searches bills from zero to one million cents and groups of one to twenty people; those are explicit test bounds, not claimed production limits. FsCheck 3's C# generator combinators live in FsCheck.Fluent, as documented in its current Gen API reference.

using FsCheck;
using FsCheck.Fluent;
using FsCheck.Xunit;

public sealed record ShareCase(int Cents, int People);

public static class ShareCases
{
    public static Arbitrary<ShareCase> Cases()
    {
        var generator =
            from cents in Gen.Choose(0, 1_000_000)
            from people in Gen.Choose(1, 20)
            select new ShareCase(cents, people);

        return Arb.From(generator, Shrink);
    }

    private static IEnumerable<ShareCase> Shrink(ShareCase value)
    {
        if (value.Cents > 0)
            yield return value with { Cents = 0 };
        if (value.Cents > 1)
        {
            yield return value with { Cents = value.Cents / 2 };
            yield return value with { Cents = 1 };
        }
        if (value.People > 1)
            yield return value with { People = 1 };
        if (value.People > 2)
            yield return value with { People = 2 };
    }
}

public sealed class BillSplitterProperties
{
    [Property(Arbitrary = new[] { typeof(ShareCases) }, MaxTest = 500)]
    public bool Shares_preserve_the_bill(ShareCase input)
    {
        var shares = BillSplitter.Split(input.Cents, input.People);

        return shares.Sum(x => (long)x) == input.Cents;
    }
}

This is an executable search, not a proof over every integer. Five hundred successful cases mean the property held for the generated sample. They do not mean all bills are correct. A broad generator makes discovery possible; a precise property makes a discovered failure meaningful.

Suppose the generated input is 734 cents and seven people. The helper returns seven shares of 104 cents, so six cents vanish. That is already a useful failure. But a smaller case is easier to recognize: one cent shared between two people produces two zeroes.

Our shrinker proposes smaller inputs while preserving the domain. Zero cents and one recipient are valid candidates, even though they do not reproduce this bug. FsCheck checks the candidates and continues with ones that still fail. Every candidate reduces a value, avoiding a cycle that keeps proposing the same case. The Arb API accepts both the generator and shrinker; constructing an arbitrary from only a generator provides no shrinking.

The pair (1, 2) is a compact explanation for this defect, not a promised transcript of every run. Shrinking follows the candidates your shrinker offers. It does not establish the globally smallest counterexample under every imaginable definition of size.

Keep the failing input and runner replay information when a CI run fails. Reproduce it using the same package version and configuration, then retain a named regression example. A seed is useful for investigation, but the explicit example communicates the business mistake long after the generator has changed.

Replace the helper's return statement with quotient-and-remainder allocation:

var shares = new int[people];
var baseShare = cents / people;
var remainder = cents % people;

for (var i = 0; i < people; i++)
    shares[i] = baseShare + (i < remainder ? 1 : 0);

return shares;

The repaired helper preserves the bill, but that property alone would also accept an implementation that gives everything to the first person. Add the other invariants as separate properties, each with the same attribute and generator. Check shares.Length == input.People, require every share to be nonnegative, and require shares.Max() - shares.Min() <= 1. Separate failures tell you whether the code lost money, lost recipients, or distributed the amount unfairly.

Then preserve the ordering decision as an ordinary example:

[Xunit.Fact]
public void Remainder_cents_go_to_the_first_recipients()
{
    var shares = BillSplitter.Split(cents: 5, people: 3);

    Xunit.Assert.Equal(new[] { 2, 2, 1 }, shares);
}

There is no competition between examples and properties. Examples give particularly important decisions names. Properties explore whether those decisions remain coherent across inputs.

Uniform random values are a starting point, not a model of your users. If production bills often have one recipient, the generated suite should regularly exercise that case. If groups can exceed the amount in cents, deliberately include those cases. If the implementation accepts int.MaxValue, an explicit boundary example should cover it even though this generator stops at one million.

Do not generate arbitrary integers and discard almost all of them with preconditions. A test that rejects most candidates spends its budget proving little. Construct valid data directly, and create a separate property or example suite for invalid input behavior. The same rule applies to dates, graphs, and account transfers: validity belongs in the generator, while the expected response to invalidity deserves its own specification.

Also resist round-trip properties as your only oracle. An encoder and decoder can share a mistake and still undo each other perfectly. Pair the round trip with known-format examples or an independent reference. For a sorting function, ordered output alone accepts a function that always returns an empty array; preserving the input's elements is another necessary property.

Property-based testing changes the source of test data, not the need to choose a meaningful observation. The same weakness exposed by mutation testing appears here: a thousand generated cases with a weak assertion can miss the same wrong answer.

Katabench's Test Writing track gives you a correct subject and authored planted-bug variants. Your suite must pass against the correct implementation and fail against enough bugs. The grading guide explains that feedback. Those exercises develop the underlying skill: identify what must remain true and choose an assertion that notices when it stops being true.

Use FsCheck in your own test project to extend that habit across generated inputs. Begin with one pure function and one conservation rule. When the runner finds a counterexample, shrink it into an explanation, add the regression example, and repair the promise that was actually broken.