Understanding Invariants in DbC

Design by Contract (DbC) is a software design approach introduced by Bertrand Meyer¹. DbC is influenced by the clear rules and responsibilities outlined in business contracts, similar to agreements between a client and a supplier. At its core, DbC involves defining a set of agreements, or contracts, between different parts of a software system. These contracts -comprising preconditions, postconditions, and invariants –  act as a formal agreement that each component must adhere to during runtime.

We already discussed pre-condition and post-condition in previous post. This post focuses on invariants.

Invariants are conditions that remain unchanged throughout the execution of a program. These are critical for maintaining the integrity of the system, preventing unexpected side effects

Examples of Invariants

1. Class Invariants:
   • In a class representing a stack data structure, an invariant could be that the size of the stack is never negative.
   • In a class representing a bank account, an invariant could be that the balance is always non-negative.
2. Loop Invariants:
   • In a loop that calculates the sum of elements in an array, an invariant could be that the sum computed so far is always accurate.
   • In a binary search algorithm, an invariant could be that the search interval always contains the target value.
3. Thread Safety Invariants:
   • In a multi-threaded program, an invariant could be that shared data structures are always accessed safely by multiple threads.
   • In a concurrent queue implementation, an invariant could be that the queue remains in a consistent state even when accessed concurrently by multiple threads.
4. Database Invariants:
   • In a database schema representing employee records, an invariant could be that every employee has a unique employee ID.
   • In a database table representing orders, an invariant could be that the total order amount is always non-negative.
5. Graph Invariants:
   • In a graph data structure representing a tree, an invariant could be that there are no cycles.
   • In a directed graph, an invariant could be that the graph remains strongly connected.

These examples illustrate how invariants help maintain the correctness, consistency, and integrity of various types of systems and data structures in programming.

Why are Invariants Important in DbC?

The use of invariants in DbC contributes significantly to the overall effectiveness of the approach in several ways:

1. Clarity and Documentation: Invariants serve as explicit statements of the expected behaviour and constraints of a software component. By documenting these constraints, invariants enhance the clarity of the software’s specification, making it easier for developers to understand and reason about the component’s behaviour.
2. Specification and Verification: Invariants provide a formal specification of the state that a software component must maintain throughout its execution. This enables developers to verify the correctness of their code by checking whether the component adheres to its invariants under various conditions.
3. Contract Enforcement: Invariants complement preconditions and postconditions in defining the contract between different software components. By enforcing invariants, DbC helps ensure that components interact with each other in a predictable and consistent manner, reducing the likelihood of errors and unexpected behaviour.
4. Debugging and Testing: Invariants serve as valuable checkpoints during debugging and testing, helping developers identify violations of expected constraints and diagnose potential issues in the software’s behaviour. By checking invariants, developers can detect and address errors early in the development process.
5. Maintainability and Evolution: Invariants facilitate software maintenance and evolution by providing a clear understanding of the fundamental properties and constraints of a software component. As the software evolves over time, invariants serve as a stable foundation for making changes and modifications while preserving the overall integrity and correctness of the system.

Overall, the use of invariants in DbC enhances the reliability, maintainability, and correctness of software systems by formalising the expected behaviour and constraints of software components and facilitating rigorous specification, verification, and enforcement of contracts between components.

Code Example using Invariant

In Design by Contract (DbC), documenting invariants in code involves specifying the conditions that must hold true for an object or system at all times. In Python, you can document class invariants using comments to describe the invariant and where it is enforced. However, unlike preconditions and postconditions, there’s no built-in syntax for formally specifying invariants in Python. Instead, developers typically use comments or docstrings to document them.

class BankAccount:
    def __init__(self, initial_balance):
        """
        Constructor for BankAccount class.

        Precondition:
            - initial_balance: Numeric value representing the initial balance of the account.
        Postcondition:
            - Initializes a new BankAccount object with the specified initial_balance.
        """
        self._balance = initial_balance
    
    @property
    def balance(self):
        """
        Getter method for the balance property.

        Postcondition:
            - Returns the current balance of the account.
        """
        return self._balance
    
    def deposit(self, amount):
        """
        Method to deposit funds into the account.

        Precondition:
            - amount: Numeric value representing the amount to be deposited. Must be non-negative.
        Postcondition:
            - Increases the account balance by the specified amount.
        """
        self._balance += amount
    
    def withdraw(self, amount):
        """
        Method to withdraw funds from the account.

        Precondition:
            - amount: Numeric value representing the amount to be withdrawn. Must be non-negative.
            - Account balance must be sufficient to cover the withdrawal.
        Postcondition:
            - Decreases the account balance by the specified amount.
        Raises:
            - ValueError: If the withdrawal amount exceeds the account balance.
        """
        if amount > self._balance:
            raise ValueError("Insufficient funds")
        self._balance -= amount

    def __setattr__(self, attr, value):
        """
        Setter method for attributes, enforcing the invariant that the balance is always non-negative.

        Precondition:
            - attr: Name of the attribute being set.
            - value: Value to set for the attribute.
        Postcondition:
            - If setting the balance attribute, ensures that the value is non-negative.
        Raises:
            - ValueError: If trying to set a negative balance directly.
        """
        if attr == '_balance' and value < 0:
            raise ValueError("Balance cannot be negative")
        super().__setattr__(attr, value)

    # Class invariant: Balance is always non-negative
    # Documenting the invariant
    # This ensures that the balance of the bank account always remains non-negative.
    # Enforced within the __setattr__ method.

In this example, the class invariant is documented using comments. The comment explains what the invariant is and where it is enforced (in the __setattr__ method). While this approach is informal, it helps communicate the expected behaviour of the class to other developers

1. Meyer, Bertrand. “Applying design by contract” Computer 25.10 (1992): 40-51 ↩︎