C++ Contracts

Formal specifications for function behavior and correctness (Future C++)

📋 What are C++ Contracts?

C++ Contracts are formal specifications that express function preconditions, postconditions, and assertions directly in code. They improve documentation, enable optimizations, and catch bugs early through automatic verification.


// Future C++ contracts syntax (proposed)
int divide(int a, int b)
    pre: b != 0                    // Precondition
    post r: r == a / b             // Postcondition
{
    return a / b;
}

// Contract violation = program termination or exception
                                    

Benefits:

✅ Self-documenting code

✅ Automatic verification

✅ Better optimization opportunities

Contract Types

📥

Preconditions

Requirements for function inputs

void func(int x)
    pre: x > 0
📤

Postconditions

Guarantees about function outputs

int square(int x)
    post r: r >= 0
✅

Assertions

Runtime checks within functions

assert: index < size;
// Check condition at runtime
🔧

Optimization

Compiler can assume contracts true

// Compiler knows x > 0
// Can optimize accordingly

🔹 Current Alternative: assert

Before concepts, runtime checks like assert were used to enforce conditions. Assertions halt execution if a boolean expression fails, aiding debugging. However, they operate at runtime (often removed in release builds) and lack the compile‑time, type‑level guarantees that concepts provide, making them less robust for generic programming.

#include <cassert>
#include <iostream>
#include <stdexcept>

// Manual precondition checking
int divide(int a, int b) {
    // Precondition: b must not be zero
    if (b == 0) {
        throw std::invalid_argument("Division by zero");
    }
    
    int result = a / b;
    
    // Postcondition check (manual)
    assert(result * b == a || (a % b != 0));
    
    return result;
}

int factorial(int n) {
    // Precondition
    assert(n >= 0);
    
    if (n <= 1) return 1;
    
    int result = 1;
    for (int i = 2; i <= n; ++i) {
        result *= i;
    }
    
    // Postcondition: result should be positive
    assert(result > 0);
    
    return result;
}

int main() {
    try {
        std::cout << "10 / 2 = " << divide(10, 2) << std::endl;
        std::cout << "5! = " << factorial(5) << std::endl;
        
        // This will throw
        // divide(10, 0);
    } catch (const std::exception& e) {
        std::cout << "Error: " << e.what() << std::endl;
    }
    
    return 0;
}

Output:

10 / 2 = 5

5! = 120

🔹 Custom Contract Macros

Developers often create macros to emulate design‑by‑contract, documenting preconditions and postconditions. These macros expand to assertions or conditional logic, improving code documentation and error checking. While not part of the language, they formalize expectations and can be toggled for testing versus deployment.

#include <iostream>
#include <stdexcept>

// Custom contract macros
#define REQUIRES(cond) \
    if (!(cond)) throw std::invalid_argument("Precondition failed: " #cond)

#define ENSURES(cond) \
    if (!(cond)) throw std::logic_error("Postcondition failed: " #cond)

// Array bounds-safe access
template<typename T, size_t N>
class SafeArray {
private:
    T data[N];
    
public:
    T& at(size_t index) {
        REQUIRES(index < N);  // Precondition
        
        T& result = data[index];
        
        // Postcondition: returned reference is valid
        ENSURES(&result >= data && &result < data + N);
        
        return result;
    }
    
    size_t size() const {
        return N;
    }
};

// Safe square root
double safe_sqrt(double x) {
    REQUIRES(x >= 0.0);  // Can't take sqrt of negative
    
    double result = std::sqrt(x);
    
    ENSURES(result >= 0.0);  // Result must be non-negative
    ENSURES(std::abs(result * result - x) < 0.0001);  // Accuracy check
    
    return result;
}

int main() {
    try {
        SafeArray<int, 5> arr;
        arr.at(0) = 42;
        std::cout << "arr[0] = " << arr.at(0) << std::endl;
        
        std::cout << "sqrt(16) = " << safe_sqrt(16.0) << std::endl;
        
        // This will fail precondition
        // safe_sqrt(-1.0);
        
    } catch (const std::exception& e) {
        std::cout << "Contract violation: " << e.what() << std::endl;
    }
    
    return 0;
}

Output:

arr[0] = 42

sqrt(16) = 4

🔹 Future Contract Syntax

Proposed contract syntax would allow annotating functions with preconditions, postconditions, and assertions. These compile‑time verified contracts would enable optimizations and static analysis, making programs faster and more reliable. Contracts formally specify obligations, bridging documentation and enforcement.

Compiler‑verified contracts ensure correctness before runtime. By analyzing annotated conditions, compilers could eliminate redundant checks, warn about violations, and even guide optimization paths. This transforms informal comments into active, trusted specifications that enhance both safety and performance.

Automatic optimization based on contracts allows compilers to assume proven conditions hold. For example, a contract guaranteeing a pointer is non‑null eliminates null checks. This reduces overhead while maintaining safety, as violations are caught during compilation or testing, not in production.

Clear function specifications via contracts improve API documentation and usability. Callers see exact requirements and guarantees, reducing misuse. Integrated into the language, contracts become a single source of truth for function behavior, aiding tools like IDEs and static analyzers.

// PROPOSED FUTURE SYNTAX - Not yet in C++
#include <vector>
#include <algorithm>

// Binary search with contracts
template<typename T>
int binary_search(const std::vector<T>& vec, const T& target)
    pre: std::is_sorted(vec.begin(), vec.end())  // Must be sorted
    post result: (result == -1) || (vec[result] == target)  // Correct result
{
    int left = 0, right = vec.size() - 1;
    
    while (left <= right) {
        int mid = left + (right - left) / 2;
        
        // Loop invariant
        assert: left >= 0 && right < vec.size();
        
        if (vec[mid] == target) {
            return mid;
        } else if (vec[mid] < target) {
            left = mid + 1;
        } else {
            right = mid - 1;
        }
    }
    
    return -1;  // Not found
}

// Safe array access
template<typename T>
T& safe_access(std::vector<T>& vec, size_t index)
    pre: index < vec.size()                    // Valid index
    post result: &result == &vec[index]        // Correct reference
{
    return vec[index];
}

// This is conceptual - not yet available in C++

Conceptual Benefits:

✅ Compiler-verified contracts

✅ Automatic optimization

✅ Clear function specifications

✅ Better testing and debugging

🧠 Test Your Knowledge

What is a precondition in a contract?