Consider this function:
// Adds two numbers safely
int add(int a, int b) {
return a + b;
}The comment says “safely.” The code doesn’t check for overflow. When a + b exceeds INT_MAX, the result is undefined behaviour - not just a wrong answer, but a license for the compiler to do anything it wants.
The comment lied. And there’s no mechanism to detect the lie.
This isn’t a contrived example. Production codebases are filled with comments that describe what the author intended, not what the code guarantees. Comments rot as code evolves. Nobody updates the “safely” comment when a rushed bug fix removes the overflow check. Six months later, a new engineer trusts the comment and builds a system that crashes in production.
Contracts offer an alternative: documentation that can’t lie because it’s enforced by the code itself.
What Contracts Actually Are
A contract is a formal specification of what a function requires and what it guarantees. The terminology comes from design-by-contract, pioneered by Bertrand Meyer in Eiffel, but the concept predates any programming language - it’s just mathematics applied to software.
A complete contract has three components:
Preconditions (PRE): What must be true before the function is called. These are the caller’s obligations.
Postconditions (POST): What will be true after the function returns, assuming preconditions were met. These are the function’s guarantees.
Invariants (INV): What must remain true throughout the function’s execution and across all calls. These are the system’s consistency rules.
Here’s the “safe add” function with an actual contract:
/*
* PRE: overflow != NULL
* POST: If (a + b) would overflow int32_t, *overflow = true and returns INT32_MAX or INT32_MIN
* POST: If no overflow, *overflow = false and returns exact result a + b
* INV: Function is pure - no side effects except writing to *overflow
*/
int32_t safe_add(int32_t a, int32_t b, bool *overflow) {
// Check for positive overflow
if ((b > 0) && (a > INT32_MAX - b)) {
*overflow = true;
return INT32_MAX;
}
// Check for negative overflow
if ((b < 0) && (a < INT32_MIN - b)) {
*overflow = true;
return INT32_MIN;
}
*overflow = false;
return a + b;
}This contract is precise enough to verify. A test can check that when a = INT32_MAX and b = 1, the function sets *overflow = true and returns INT32_MAX. Another test can verify that safe_add(2, 3, &ovf) returns 5 with ovf = false.
The contract isn’t aspirational documentation - it’s a specification that tests enforce.
Why Comments Fail
Comments and contracts serve different purposes, but codebases often use comments where contracts are needed.
Comments Describe Intent
// Calculate the average of values in the array
double average(double *values, int count) {
double sum = 0;
for (int i = 0; i < count; i++) {
sum += values[i];
}
return sum / count;
}This comment tells you what the function is for, but nothing about what it requires or guarantees:
- What if
valuesis NULL? - What if
countis zero? (Division by zero - undefined behaviour) - What if
countis negative? - What if the sum overflows?
- What if the array contains NaN?
The comment says “calculate the average” but the code might crash, return infinity, return NaN, or return garbage. A maintainer reading this comment has no idea which edge cases are handled.
Comments Rot
Code evolves. Comments don’t.
// Returns the user's full name, or "Unknown" if not found
char* get_user_name(int user_id) {
User *user = lookup_user(user_id);
if (user == NULL) {
return NULL; // Changed in v2.3 to return NULL instead
}
return user->full_name;
}The comment says “Unknown” but the code returns NULL. Someone changed the behaviour but not the documentation. Any code relying on the comment will dereference NULL and crash.
Comments Can’t Be Tested
There’s no automated way to verify that a comment matches the code’s actual behaviour. You can lint for missing comments, but not for lying ones. Code review might catch discrepancies, but code review is fallible and doesn’t scale.
Contracts, expressed as preconditions and postconditions, can be mechanically tested. The test suite becomes a formal verification that the contract holds.
Contracts in Practice
The c-from-scratch framework uses contracts throughout. Here’s how they appear in a real module:
Header File Contracts
The public interface declares contracts in header comments:
/**
* baseline_update - Process a new input value
*
* PRE: ctx != NULL
* PRE: ctx initialised via baseline_init()
* PRE: timestamp > ctx->last_timestamp (monotonic time)
* PRE: value is finite (not NaN or Inf)
*
* POST: ctx->state updated according to FSM rules
* POST: If value is anomalous, ctx->anomaly_count incremented
* POST: If in MONITORING state, EMA and variance updated
* POST: Returns BASELINE_OK on success, error code on precondition violation
*
* INV: O(1) time complexity
* INV: O(1) space complexity (no allocation)
* INV: Deterministic (same inputs -> same outputs)
*/
int baseline_update(baseline_t *ctx, double value, uint64_t timestamp);This contract tells you everything you need to call the function correctly:
- What you must provide (non-null, initialised context, monotonic time, finite value)
- What you’ll get back (updated state, incremented counters, specific return codes)
- What’s guaranteed about execution (bounded time, bounded space, deterministic)
Implementation Enforces Contracts
The implementation’s first job is to verify preconditions:
int baseline_update(baseline_t *ctx, double value, uint64_t timestamp) {
// Verify preconditions
if (ctx == NULL) {
return BASELINE_ERR_NULL;
}
if (timestamp <= ctx->last_timestamp) {
return BASELINE_ERR_TEMPORAL;
}
if (!isfinite(value)) {
return BASELINE_ERR_DOMAIN;
}
// Preconditions satisfied - proceed with update
// ...
}This pattern - check preconditions first, return error codes on violation - ensures that:
- The function never operates on invalid input
- Callers get explicit notification of violations
- The system fails safely rather than corrupting state
Tests Verify Contracts
Each contract clause becomes one or more tests:
// Test: PRE ctx != NULL
void test_null_context_rejected(void) {
int result = baseline_update(NULL, 1.0, 1000);
assert(result == BASELINE_ERR_NULL);
}
// Test: PRE timestamp > ctx->last_timestamp
void test_non_monotonic_timestamp_rejected(void) {
baseline_t ctx;
baseline_init(&ctx, &default_config);
baseline_update(&ctx, 1.0, 1000);
int result = baseline_update(&ctx, 2.0, 500); // Earlier timestamp
assert(result == BASELINE_ERR_TEMPORAL);
}
// Test: PRE value is finite
void test_nan_rejected(void) {
baseline_t ctx;
baseline_init(&ctx, &default_config);
int result = baseline_update(&ctx, NAN, 1000);
assert(result == BASELINE_ERR_DOMAIN);
}
// Test: POST deterministic
void test_determinism(void) {
baseline_t ctx1, ctx2;
baseline_init(&ctx1, &default_config);
baseline_init(&ctx2, &default_config);
// Same inputs
baseline_update(&ctx1, 1.0, 1000);
baseline_update(&ctx2, 1.0, 1000);
// Must produce same state
assert(ctx1.state == ctx2.state);
assert(ctx1.ema == ctx2.ema);
assert(ctx1.variance == ctx2.variance);
}When these tests pass, the contracts are verified. When code changes break a contract, tests fail. The documentation can’t lie because the tests enforce it.
The Contract Hierarchy
Contracts exist at multiple levels, from individual functions to entire systems.
Function-Level Contracts
The most granular level. Each function specifies what it requires and guarantees:
// PRE: 0 <= index < array_size
// POST: Returns array[index]
// INV: No side effects
int get_element(int *array, int index, int array_size);Module-Level Invariants
Contracts that apply across all functions in a module:
/*
* MODULE INVARIANT: The baseline_t struct is always in a valid state
*
* - state ∈ {LEARNING, MONITORING, FAULT}
* - If state == MONITORING, then sample_count >= min_samples
* - variance >= 0 (never negative)
* - ema is finite (never NaN or Inf) when state != FAULT
*/Every function that modifies baseline_t must preserve these invariants. Tests verify the invariants hold before and after each operation.
System-Level Contracts
Contracts between components. The Init-Update-Status-Reset pattern described in c-from-scratch is itself a system-level contract:
/*
* SYSTEM CONTRACT: Init-Update-Status-Reset Lifecycle
*
* 1. init() must be called before any other function
* 2. update() is the only function that modifies state
* 3. status() is a pure function (no side effects)
* 4. reset() returns module to post-init state
* 5. reset() is safe to call at any time
* 6. After reset(), module behaves as if freshly initialised
*/Any module implementing this pattern can be composed with any other such module. The contract guarantees interoperability.
Contracts vs. Assertions
Some languages provide assert() for runtime checks. How do contracts differ?
Assertions Check Implementation Details
void process_buffer(char *buf, int len) {
assert(len > 0); // Catch programmer errors
assert(buf != NULL);
// ... implementation
}These assertions help during debugging but disappear in release builds (when NDEBUG is defined). They’re not part of the interface - they’re implementation sanity checks.
Contracts Define the Interface
/*
* PRE: len > 0
* PRE: buf != NULL
*/
int process_buffer(char *buf, int len) {
if (len <= 0) return ERR_INVALID_LENGTH;
if (buf == NULL) return ERR_NULL_POINTER;
// ... implementation
}This contract is part of the function’s specification. The checks remain in release builds because they’re part of correct operation, not debugging aids. The caller can rely on getting an error code rather than undefined behaviour.
When to Use Each
Use assertions for: Internal consistency checks, conditions that indicate bugs in this code, checks that can be disabled without affecting correctness.
Use contracts for: Interface specifications, conditions that callers must satisfy, checks that must remain active in production.
In safety-critical systems, assertions are often prohibited because they can be disabled. Contracts enforced by explicit checks are required.
Contracts Enable Composition
When components have well-defined contracts, they can be composed predictably.
Consider two modules, each following the Init-Update-Status-Reset pattern:
// Module A: Temperature monitor
// POST: Returns TEMP_OK if reading is valid
// POST: Returns TEMP_FAULT if sensor failure detected
int temp_update(temp_t *ctx, double reading, uint64_t time);
// Module B: Pressure monitor
// POST: Returns PRESS_OK if reading is valid
// POST: Returns PRESS_FAULT if sensor failure detected
int press_update(press_t *ctx, double reading, uint64_t time);A system-level monitor can compose these:
int system_update(system_t *sys, sensor_data_t *data, uint64_t time) {
int temp_result = temp_update(&sys->temp, data->temperature, time);
int press_result = press_update(&sys->press, data->pressure, time);
// Compose results according to system contract
if (temp_result == TEMP_FAULT || press_result == PRESS_FAULT) {
sys->state = SYSTEM_FAULT;
return SYSTEM_FAULT;
}
return SYSTEM_OK;
}Because each module’s contracts are known, the composition’s behaviour is predictable. The system-level contract can be derived from the component contracts.
This is how safety-critical systems are built: verified components with known contracts, composed into verified systems. The alternative - hoping that components interact correctly - doesn’t scale and can’t be certified.
Contracts in Documentation
For projects with external users, contracts belong in documentation as well as code:
API Documentation
## baseline_update
Updates the baseline monitor with a new value.
### Parameters
- `ctx`: Pointer to initialised baseline_t structure
- `value`: New measurement value (must be finite)
- `timestamp`: Current time in nanoseconds (must be monotonically increasing)
### Returns
- `BASELINE_OK` (0): Success
- `BASELINE_ERR_NULL` (-1): ctx was NULL
- `BASELINE_ERR_TEMPORAL` (-2): timestamp was not greater than previous
- `BASELINE_ERR_DOMAIN` (-3): value was NaN or infinite
### Contract
**Preconditions:**
- `ctx != NULL`
- `ctx` has been initialised via `baseline_init()`
- `timestamp > ctx->last_timestamp`
- `isfinite(value)`
**Postconditions:**
- State machine updated according to current state and value
- If anomaly detected, `ctx->anomaly_count` incremented
- Returns appropriate status code
**Invariants:**
- O(1) time complexity
- O(1) space complexity
- Deterministic executionThis documentation can’t rot because it matches the code’s actual behaviour - the tests verify it.
From Proofs to Code
Contracts bridge the gap between mathematical specification and implementation, as discussed in From Proofs to Code: Mathematical Transcription in C.
The mathematical model defines what should happen:
State transition: MONITORING + anomaly → increment counter
Formally: anomaly(v) ∧ state = MONITORING → counter' = counter + 1The contract specifies the function’s obligations:
// POST: If value is anomalous and state == MONITORING, anomaly_count incrementedThe implementation fulfills the contract:
if (is_anomaly(ctx, value) && ctx->state == MONITORING) {
ctx->anomaly_count++;
}The test verifies the contract:
void test_anomaly_increments_counter(void) {
baseline_t ctx;
baseline_init(&ctx, &config);
advance_to_monitoring(&ctx); // Helper to reach MONITORING state
uint32_t count_before = ctx.anomaly_count;
baseline_update(&ctx, ANOMALOUS_VALUE, next_time());
assert(ctx.anomaly_count == count_before + 1);
}This chain - math → contract → code → test - is traceable. An auditor can verify that requirements flow through to implementation.
Practical Contract Patterns
The Guard Pattern
Check preconditions immediately, return on violation:
int process(context_t *ctx, input_t input) {
// Guards - check all preconditions first
if (ctx == NULL) return ERR_NULL;
if (!is_valid_input(input)) return ERR_INVALID;
if (ctx->state == STATE_FAULT) return ERR_FAULT;
// All preconditions satisfied - do the work
// ...
}Guards make precondition checking explicit and consistent. The function’s “happy path” only executes when all preconditions are met.
The State Machine Pattern
Model valid states and transitions explicitly:
typedef enum {
STATE_INIT,
STATE_READY,
STATE_RUNNING,
STATE_FAULT
} state_t;
// CONTRACT: Valid transitions
// INIT -> READY (via initialise)
// READY -> RUNNING (via start)
// RUNNING -> READY (via stop)
// ANY -> FAULT (via error)
// FAULT -> INIT (via reset)
int transition(context_t *ctx, event_t event) {
switch (ctx->state) {
case STATE_INIT:
if (event == EVENT_INIT_COMPLETE) {
ctx->state = STATE_READY;
return OK;
}
break;
// ... other transitions
}
return ERR_INVALID_TRANSITION;
}The state machine is the contract. Invalid transitions return errors rather than corrupting state.
The Result Pattern
Return structured results that capture success, failure, and context:
typedef struct {
int status; // OK or error code
double value; // Result if OK
const char *message; // Human-readable status
} result_t;
// CONTRACT:
// If result.status == OK, result.value contains valid output
// If result.status != OK, result.message describes the failure
result_t calculate(double input) {
if (!isfinite(input)) {
return (result_t){ERR_DOMAIN, 0, "Input must be finite"};
}
double output = /* calculation */;
if (!isfinite(output)) {
return (result_t){ERR_OVERFLOW, 0, "Calculation overflowed"};
}
return (result_t){OK, output, "Success"};
}Callers can’t accidentally use invalid results because the contract ties validity to the status code.
Conclusion
Comments describe what programmers hope code does. Contracts specify what code must do - and tests verify that it does.
The shift from comments to contracts isn’t just better documentation. It’s a different way of thinking about software:
- Functions have obligations (postconditions), not just behaviours
- Callers have obligations (preconditions), not just inputs
- Systems have consistency rules (invariants), not just states
This thinking leads naturally to code that can be reasoned about, tested systematically, and trusted in production. It’s the foundation of safety-critical development, but it benefits any codebase where correctness matters.
Comments will always have a place - explaining why decisions were made, providing context, helping humans understand code. But for specifying what code guarantees, contracts are the tool that can’t lie.
The c-from-scratch framework provides working examples of contract-based development. The patterns described here - guards, state machines, structured results - appear throughout. For a structured introduction to this methodology, “C From Scratch” covers contracts from first principles.
As with any engineering practice, the appropriate level of formality depends on context. Not every function needs a full contract specification. But understanding what contracts are and when to use them is essential knowledge for engineers building systems that matter.
Documentation should tell the truth. Contracts make sure it does.