Design by Contract in TypeScript and C#

Suppose a warehouse has ten items available and a customer reserves three. The result should say “seven remaining, three reserved.” That sounds too obvious to document, until a refactor reserves two, an invalid quantity increases the stock, or a caller treats “out of stock” as a successful reservation.

A signature such as reserveStock(available: number, quantity: number) leaves those rules unstated. Both arguments can be numbers while the request makes no sense. Design by Contract puts the rules beside the operation and assigns responsibility for each one.

Bertrand Meyer developed Design by Contract as a central part of Eiffel. Its preconditions, postconditions, and invariants describe the agreement between a caller and a routine. We can apply that design discipline in TypeScript and C# with ordinary functions, even though these helpers do not supply Eiffel’s full contract machinery.

The complete, compilable examples are in 8exgh/design-by-contract on GitHub, with Jest tests for TypeScript and xUnit tests for C#. Clone the repository or use the download at the end of this article.

Write the agreement before the algorithm

Our function calculates a reservation from one snapshot of available stock. It returns a new value containing the remaining and reserved quantities. It performs no database writes. That scope lets us express the core rule without hiding storage, concurrency, or network behaviour inside the example.

The two postconditions work together. “Counts are nonnegative” would accept seven remaining and two reserved. “Stock is conserved” alone would accept eight remaining and two reserved. Requiring the requested amount and conservation rules out both mistakes.

The caller has to meet the preconditions; the function still checks them at entry in our implementation. If the call is valid and the function returns normally, the caller can rely on its postconditions. A violation identifies an internal disagreement that should be diagnosed, rather than quietly converted into a plausible result.

The assertions belong inside the function. A failed precondition means its caller broke the internal API’s requirements. A failed postcondition means the implementation broke its promise. Both are bugs. The postcondition runs after calculating the candidate result and before returning it; code placed after return would never run. These helpers throw an exception so an incorrect result cannot escape as a successful return.

TypeScript: small helpers with assertion signatures

Each helper accepts a Boolean condition and a message describing the rule. The three names make the responsibility visible, and the error’s kind distinguishes a bad call, an incorrect result, and invalid state.

export type ContractKind = "precondition" | "postcondition" | "invariant";

export class ContractViolation extends Error {
  constructor(readonly kind: ContractKind, rule: string) {
    super(`${kind}: ${rule}`);
    this.name = "ContractViolation";
  }
}

export function requires(condition: boolean, rule: string): asserts condition {
  if (!condition) throw new ContractViolation("precondition", rule);
}

export function ensures(condition: boolean, rule: string): asserts condition {
  if (!condition) throw new ContractViolation("postcondition", rule);
}

export function invariant(condition: boolean, rule: string): asserts condition {
  if (!condition) throw new ContractViolation("invariant", rule);
}

The asserts condition return annotation tells TypeScript that the condition is true if execution continues past the call. It supports control-flow narrowing, such as treating a nullable name as a string after checking it. The annotation supplies compiler information; the throw supplies the runtime check. An assertion signature with an incorrect implementation can mislead the compiler. TypeScript documents this as an assertion function.

Here is the complete reservation implementation using those helpers:

import { requires, ensures, invariant } from "./contracts.js";

export type Reservation = Readonly<{
  remaining: number;
  reserved: number;
}>;

export function assertReservation(value: Reservation): void {
  invariant(
    Number.isSafeInteger(value.remaining) && value.remaining >= 0,
    "remaining stock must be a nonnegative safe integer",
  );
  invariant(
    Number.isSafeInteger(value.reserved) && value.reserved >= 0,
    "reserved stock must be a nonnegative safe integer",
  );
}

export function reserveStock(available: number, quantity: number): Reservation {
  // PRECONDITIONS: a failure is a bug in the caller of this internal function.
  requires(
    Number.isSafeInteger(available) && available >= 0,
    "available stock must be a nonnegative safe integer",
  );
  requires(
    Number.isSafeInteger(quantity) && quantity > 0,
    "quantity must be a positive safe integer",
  );
  requires(quantity <= available, "quantity must not exceed available stock");

  // WORK: calculate a candidate result without changing shared state.
  const result = Object.freeze({
    remaining: available - quantity,
    reserved: quantity,
  });

  // POSTCONDITIONS: a failure is a bug in this implementation.
  // Check after the work, before returning the result to the caller.
  assertReservation(result);
  ensures(result.reserved === quantity, "reserve exactly the requested quantity");
  ensures(
    result.remaining + result.reserved === available,
    "stock must be conserved",
  );
  return result;
}

Number.isSafeInteger matters here. TypeScript’s number includes fractions, NaN, and infinities. JavaScript also has a limit beyond which integer arithmetic loses the guarantees we need. The accepted nonnegative range in this example ends at Number.MAX_SAFE_INTEGER, or 9,007,199,254,740,991. The safe-integer check excludes values outside that domain.

Every check runs before the result returns. The subtraction is safe because quantity is positive and no greater than available stock. The returned object is frozen, so a consumer cannot overwrite its two numeric fields. A shallow freeze is enough for this flat object; nested mutable data would need its own treatment.

reserveStock(10, 3);
// { remaining: 7, reserved: 3 }

reserveStock(10, 10);
// { remaining: 0, reserved: 10 }

reserveStock(10, 11);
// Throws ContractViolation:
// precondition: quantity must not exceed available stock

C#: the same agreement, checked in Release too

The C# version uses the same three helpers and a dedicated exception carrying the failure kind. These are ordinary methods in our own Dbc class. They throw whenever a condition is false.

using System;
using System.Diagnostics.CodeAnalysis;

namespace ContractExamples;

public enum ContractKind { Precondition, Postcondition, Invariant }

public sealed class ContractViolationException : Exception
{
    public ContractKind Kind { get; }

    public ContractViolationException(ContractKind kind, string rule)
        : base($"{kind}: {rule}") => Kind = kind;
}

public static class Dbc
{
    public static void Requires([DoesNotReturnIf(false)] bool condition, string rule)
    {
        if (!condition)
            throw new ContractViolationException(ContractKind.Precondition, rule);
    }

    public static void Ensures([DoesNotReturnIf(false)] bool condition, string rule)
    {
        if (!condition)
            throw new ContractViolationException(ContractKind.Postcondition, rule);
    }

    public static void Invariant([DoesNotReturnIf(false)] bool condition, string rule)
    {
        if (!condition)
            throw new ContractViolationException(ContractKind.Invariant, rule);
    }
}

DoesNotReturnIf(false) communicates to the compiler that a false condition prevents normal return. It helps nullable analysis understand a guard such as Dbc.Requires(name is not null, ...). The attribute does not insert a check or prove the arithmetic; our method body performs the check. Microsoft documents that flow-analysis contract here.

There is deliberately no DEBUG condition around these methods. Calls to Debug.Assert depend on the DEBUG compilation symbol, which typical Release builds omit. These exception-based helpers run in both configurations. The Debug class documentation explains that distinction.

namespace ContractExamples;

public readonly record struct Reservation(int Remaining, int Reserved);

public static class Stock
{
    public static void AssertReservation(Reservation value)
    {
        Dbc.Invariant(value.Remaining >= 0, "remaining stock must be nonnegative");
        Dbc.Invariant(value.Reserved >= 0, "reserved stock must be nonnegative");
    }

    public static Reservation ReserveStock(int available, int quantity)
    {
        // PRECONDITIONS: a failure is a bug in the caller of this internal method.
        Dbc.Requires(available >= 0, "available stock must be nonnegative");
        Dbc.Requires(quantity > 0, "quantity must be positive");
        Dbc.Requires(quantity <= available, "quantity must not exceed available stock");

        // WORK: calculate a candidate result without changing shared state.
        var result = new Reservation(
            Remaining: available - quantity,
            Reserved: quantity);

        // POSTCONDITIONS: a failure is a bug in this implementation.
        // Check after the work, before returning the result to the caller.
        AssertReservation(result);
        Dbc.Ensures(result.Reserved == quantity, "reserve exactly the requested quantity");
        Dbc.Ensures(
            (long)result.Remaining + result.Reserved == available,
            "stock must be conserved");
        return result;
    }
}

An int already excludes fractions, NaN, and infinity, so C# needs fewer numeric checks. Its maximum here is 2,147,483,647. The business rule matches the TypeScript example, but the two implementations intentionally have different numeric limits. The cast to long makes the postcondition’s sum safe even while inspecting an incorrect pair of int results.

Stock.ReserveStock(10, 3);
// Reservation { Remaining = 7, Reserved = 3 }

Stock.ReserveStock(10, 10);
// Reservation { Remaining = 0, Reserved = 10 }

Stock.ReserveStock(10, 11);
// Throws ContractViolationException:
// Precondition: quantity must not exceed available stock

An invariant describes valid state

A postcondition relates an operation’s result to the call that produced it. An invariant describes a valid state independently of that particular call. In our example, conservation refers to the original available argument; nonnegative counts make sense whenever we inspect a reservation.

That is why assertReservation is a separate function. Another operation that splits or combines reservations could check the same state rules while having different preconditions and postconditions. In functional code, check the returned state. In a mutable class, establish the invariant during construction and preserve it whenever public operations hand control back to callers. Eiffel’s class invariant expresses this shared obligation across routines.

The TypeScript return is frozen, and C#’s readonly record struct prevents changing that returned value in place. Neither public type makes invalid values impossible to construct elsewhere: a caller can create a negative-count object or a modified C# copy. Our guarantee is about results returned by reserveStock. Accepting externally constructed state requires validation or a type that controls construction.

We also need the state from before the operation. Here, available is already a number passed by value, so it remains the original snapshot for the conservation check. With mutable state, save the needed values before modifying it. Saving another reference to the same object does not preserve its old contents.

Bad input is expected; an internal contract violation is a bug

A shopper requesting eleven items when only ten remain is an ordinary outcome. The checkout boundary should recognise that request and return an “insufficient stock” response. It should call the strict reservation function only after satisfying its requirements.

The same applies to an empty field, a fractional quantity, or text that cannot be parsed. Parse and validate at the boundary, explain the problem to the user, and allow a correction. In TypeScript, treat incoming JSON as untrusted data even if an interface describes the desired shape. In C#, use parsing and model validation before invoking the typed domain function.

These layers can evaluate similar predicates while having different responsibilities. The boundary handles expected rejection. The inner precondition catches a programming error when a caller bypasses that boundary or supplies inconsistent state. Catching every ContractViolation and returning “out of stock” would conceal postcondition failures as well.

For a reusable .NET library, standard exceptions such as ArgumentOutOfRangeException may be the right public convention for invalid arguments. The dedicated exception here makes the teaching example’s three failure categories explicit. The important design choice is to keep expected business outcomes distinguishable from broken internal assumptions.

Test the promises and deliberately break the implementation

A contract is a statement to check on each execution that reaches it. A test supplies particular executions and verifies what happens. Tests can exercise boundaries, failure paths, and interactions; property-based tests can generate many inputs against a general property. None of those approaches becomes unnecessary because we added three helpers.

The repository’s Jest suite and xUnit suite cover an ordinary reservation, reserving all stock, each language’s upper numeric boundary, invalid arguments, invalid state, and all three failure kinds. They also check compiler narrowing after a non-null precondition. Each implementation exercises all 5,050 valid input pairs with available stock from one through one hundred. That bounded sweep is useful evidence, not exhaustive coverage of the whole input domain.

A more revealing experiment is to introduce a mistake in the calculation. Change the subtraction to addition:

// TypeScript, inside the result object:
remaining: available + quantity,

// C#, inside the Reservation constructor call:
Remaining: available + quantity,

For ten available and three requested, the buggy implementation produces thirteen remaining and three reserved. Both counts are nonnegative, and the reserved quantity is correct. The conservation postcondition still catches it: sixteen does not equal ten. The function throws stock must be conserved instead of returning the incorrect result.

I compiled the TypeScript examples in strict mode and ran Jest, ran xUnit against the C# solution in Release mode, and checked the deliberate bug in temporary copies of both implementations. The postcondition mutation script makes that experiment repeatable: it requires compilation to succeed, then verifies that Jest and xUnit fail with the specific conservation postcondition error. A compiler error or an ordinary wrong-result assertion does not count. The source shown above matches the repository revision included in the download.

Contracts can also be wrong or incomplete. If the specification forgets a fee, an ordering rule, or an identity requirement, passing its checks will not recover that missing requirement. Tests with independently chosen expected outcomes help expose those gaps. A good postcondition expresses a meaningful property of the result, rather than calling the implementation again and comparing it with itself.

Be precise about what these helpers guarantee

Successful return is the checkpoint. A postcondition after the body runs only if control reaches it. It cannot prove that a loop terminates or that an awaited operation eventually completes. Termination and time limits need their own reasoning and mechanisms. Exceptional exits also need an explicit policy for the state left behind.

Throwing does not undo work. Our function calculates a fresh value before returning it. A method that charges a card, sends a message, or commits a database write has already caused an effect. A later failed assertion does not reverse that effect. Arrange checks and transaction boundaries around the guarantees you actually need.

A snapshot is not a lock. Two callers can each read ten available and correctly calculate a reservation of seven. Both local contracts can pass while the combined reservations oversell stock. A real persistence layer must enforce the rule with an atomic conditional update, appropriate transaction isolation, or another concurrency mechanism. The pure function establishes the arithmetic for one snapshot.

Keep checks free of side effects. Conditions should inspect values, not save records, advance iterators, or modify state. These helpers evaluate their Boolean argument on every call; they do not defer an expensive query. The checks here are small. More expensive properties need a deliberate monitoring strategy, and removing a check removes its runtime protection.

Inheritance requires compatible promises. An override must continue accepting what the base contract accepted and guarantee at least what it promised. It can weaken preconditions or strengthen postconditions. These ordinary helpers do not compose inherited contracts or insert invariant checks automatically. Eiffel’s introduction explains those inheritance rules.

Try designing the blender before coding it

A small stateful exercise makes the distinctions concrete. Assume ten speed settings, numbered zero through nine, where zero means off. The blender cannot run empty, and speed changes can move by at most one setting; requesting the current speed is a permitted no-op.

• Invariant: speed is an integer from zero through nine, and an empty blender has speed zero.
• Set speed: require a valid target within one step of the old speed, and require contents for a nonzero target. Guarantee that the new speed equals the target and the contents are unchanged.
• Fill: for this design, require an empty, stopped blender. Guarantee that it is full and remains stopped.
• Empty: require a full, stopped blender. Guarantee that it is empty and remains stopped.

The fill and empty rules are explicit choices for this interface. A different interface could allow repeated calls as no-ops, provided it states that policy. Writing the contract makes these choices visible before they become accidental behaviour.

Run the examples and reuse the helpers

Start with github.com/8exgh/design-by-contract. It contains both implementations, Jest and xUnit unit tests, dependency lock files, a README, and a workflow that builds and tests both languages on pushes and pull requests. The examples were checked with TypeScript 5.9.3 and Jest on Node.js 22, and xUnit v3 on the .NET 8 SDK.

git clone https://github.com/8exgh/design-by-contract.git
cd design-by-contract

The optional archive is a snapshot of revision ce966bc. Extract it and open the design-by-contract directory. From either the clone or that extracted directory, compile TypeScript and run Jest:

npm --prefix typescript ci
npm --prefix typescript test

The test command invokes tsc in strict mode before Jest runs the compiled JavaScript. From the same repository directory, compile C# and run xUnit in Release:

dotnet restore csharp/DesignByContract.sln --locked-mode
dotnet test csharp/DesignByContract.sln --configuration Release --no-restore

After those dependencies are installed, prove that the postconditions catch the deliberately broken calculation:

node scripts/check-postconditions.mjs

Start with one function whose correctness matters. Write down what it needs, what its caller may rely on, and which state rules it must preserve. Turn those statements into cheap checks, then write tests that try to break the agreement. That small discipline makes the function easier to use, review, and change.

This walkthrough was inspired by the Design by Contract discussion in David Thomas and Andrew Hunt’s The Pragmatic Programmer, 20th Anniversary Edition. The explanations and TypeScript/C# implementations here are original worked examples. For another way to make a coding rule executable, read A Coding Standard That Fails the Build.