Contracts (Design by Contract)

Kit supports Design by Contract through preconditions and postconditions. Contracts allow you to specify invariants that must hold when functions are called and when they return, making your code more robust and self-documenting.

Introduction

Design by Contract is a programming methodology where you explicitly specify:

• Preconditions - What must be true before a function executes
• Postconditions - What must be true after a function completes

In Kit, contracts are expressed using @pre and @post annotations placed before function definitions. When a contract condition is violated, the function panics with an error message.

Basic Syntax

# Precondition syntax
@pre(condition)
@pre(condition, "error message")

# Postcondition syntax
@post(condition)
@post(condition, "error message")

# Function with contracts
@pre(x >= 0, "x must be non-negative")
square-root = fn(x) => Math.sqrt x

Preconditions

Preconditions are checked before the function body executes. They validate that the function's inputs are valid and that any required state is in place.

Validating Parameters

# Ensure input is non-negative
@pre(n >= 0, "n must be non-negative")
factorial = fn(n) =>
  if n <= 1 then 1 else n * factorial(n - 1)

# Validate string is not empty
@pre(String.length s > 0, "string cannot be empty")
first-char = fn(s) => String.at 0 s

# Validate numeric range
@pre(age >= 0 && age <= 150, "age must be between 0 and 150")
create-person = fn(name, age) => {name: name, age: age}

Preventing Division by Zero

@pre(divisor != 0, "Cannot divide by zero")
safe-divide = fn(dividend, divisor) =>
  dividend / divisor

# Usage
result = safe-divide 10 2    # => 5
result = safe-divide 10 0    # Panics: "Cannot divide by zero"

List Operations

# Ensure list is not empty before computing average
@pre(not (List.empty? list), "List cannot be empty")
average = fn(list) =>
  List.sum list / List.length list

# Ensure index is within bounds
@pre(index >= 0 && index < List.length list, "Index out of bounds")
safe-get = fn(list, index) =>
  List.at index list

Postconditions

Postconditions are checked after the function body executes. They validate that the function's result meets expected constraints. The special binding result refers to the function's return value.

Validating Return Values

# Ensure result is positive
@post(result > 0, "Result must be positive")
absolute-value = fn(x) =>
  if x >= 0 then x else -x

# Ensure result is within expected range
@post(result >= 0 && result <= 100, "Percentage must be 0-100")
calculate-percentage = fn(part, whole) =>
  (part / whole) * 100

Verifying Invariants

# Division invariant: result * divisor should equal dividend
@pre(divisor != 0, "Cannot divide by zero")
@post(result * divisor == dividend, "Division invariant violated")
integer-divide = fn(dividend, divisor) =>
  dividend / divisor

# Sorting invariant: result should be sorted
@post(List.sorted? result, "Result must be sorted")
sort-numbers = fn(numbers) =>
  List.sort numbers

Accessing Parameters in Postconditions

Postconditions can access both function parameters and the return value:

# Result length should match input length
@post(List.length result == List.length items, "Length must be preserved")
double-all = fn(items) =>
  List.map (fn(x) => x * 2) items

# Filter should not increase length
@post(List.length result <= List.length items, "Filter cannot increase length")
filter-positive = fn(items) =>
  List.filter (fn(x) => x > 0) items

Multiple Contracts

Functions can have multiple preconditions and postconditions. All conditions are checked in order - preconditions before execution, postconditions after.

# Multiple preconditions
@pre(x >= 0, "x must be non-negative")
@pre(y >= 0, "y must be non-negative")
@pre(x + y > 0, "At least one value must be positive")
weighted-average = fn(a, b, x, y) =>
  (a * x + b * y) / (x + y)

# Multiple pre and post conditions
@pre(divisor != 0, "Cannot divide by zero")
@pre(dividend >= 0, "Dividend must be non-negative")
@post(result >= 0, "Result must be non-negative")
@post(result <= dividend, "Result cannot exceed dividend")
safe-integer-divide = fn(dividend, divisor) =>
  dividend / divisor

Complex Example

# Bank account withdrawal with multiple contracts
@pre(amount > 0, "Withdrawal amount must be positive")
@pre(amount <= account.balance, "Insufficient funds")
@post(result.balance == account.balance - amount, "Balance not updated correctly")
@post(result.balance >= 0, "Balance cannot be negative")
withdraw = fn(account, amount) =>
  {balance: account.balance - amount, id: account.id}

Error Messages

Error messages are optional but highly recommended. They make debugging easier by providing context about which contract failed and why.

Without Error Messages

# Works but gives generic error on failure
@pre(n >= 0)
@post(result >= 1)
factorial = fn(n) =>
  if n <= 1 then 1 else n * factorial(n - 1)

With Descriptive Error Messages

# Clear error messages help identify issues quickly
@pre(n >= 0, "factorial requires non-negative input, got ${n}")
@post(result >= 1, "factorial result must be at least 1")
factorial = fn(n) =>
  if n <= 1 then 1 else n * factorial(n - 1)

Dynamic Error Messages

You can include parameter values in error messages using string interpolation:

@pre(age >= 0, "Age must be non-negative, got ${age}")
@pre(age <= 150, "Age ${age} exceeds maximum of 150")
create-person = fn(name, age) =>
  {name: name, age: age}

# When called with invalid input:
create-person "Alice" -5   # Panics: "Age must be non-negative, got -5"
create-person "Bob" 200    # Panics: "Age 200 exceeds maximum of 150"

When to Use Contracts

Contracts are most valuable in specific situations. Here are guidelines for when to use them effectively.

Good Use Cases

• Public API boundaries - Validate inputs from external callers
• Mathematical functions - Enforce domain constraints (e.g., non-negative for sqrt)
• Critical business logic - Ensure invariants in financial calculations
• Data transformations - Verify that transformations preserve expected properties
• Recursive functions - Validate base case conditions

# API boundary - validate external input
@pre(String.length email > 0, "Email cannot be empty")
@pre(String.contains? email "@", "Email must contain @")
register-user = fn(email, password) =>
  # ... registration logic

# Mathematical domain constraint
@pre(x > 0, "Logarithm requires positive input")
safe-log = fn(x) => Math.log x

# Business logic invariant
@pre(quantity > 0, "Order quantity must be positive")
@pre(price >= 0, "Price cannot be negative")
@post(result.total == quantity * price, "Total calculation error")
create-order-line = fn(product, quantity, price) =>
  {product: product, quantity: quantity, price: price, total: quantity * price}

When to Prefer Other Approaches

• Expected error cases - Use Result types instead of contracts for recoverable errors
• Optional values - Use Option types for values that may be absent
• Performance-critical code - Contracts add runtime overhead; consider disabling in production

# Use Result for expected errors (recoverable)
parse-int = fn(s) =>
  match String.to-int s
    | Some n -> Ok n
    | None -> Err "Invalid integer"

# Use contracts for programming errors (not recoverable)
@pre(index >= 0, "Index cannot be negative")
internal-array-access = fn(array, index) =>
  # ...

Contracts vs Tests

Contracts and tests serve complementary purposes:

Aspect	Contracts	Tests
When checked	Every function call at runtime	During test execution only
Coverage	All inputs in production	Only tested scenarios
Documentation	Self-documenting requirements	Example-based documentation
Performance	Runtime overhead	No production overhead

Use both together: contracts catch unexpected conditions in production, while tests verify specific scenarios during development.