How can you verify your code with design by contract?

1 What is DBC?

DBC is based on the analogy of a contract between a supplier and a client, where the supplier provides a service or product and the client uses it. This contract defines the obligations and benefits of both parties, such as the supplier delivering the product on time and in good condition, and the client paying the agreed price. If either party violates the contract, the other party has the right to terminate the relationship or seek compensation. In object oriented design, this contract consists of three elements: preconditions, postconditions, and invariants. Preconditions are conditions that must be met by the client before calling a method; postconditions are conditions that must be met by the supplier after returning from a method; and invariants are conditions that must be maintained by the supplier at all times. By defining these elements, you can better understand, test, and reuse your code by specifying its responsibilities and assumptions.

2 How to implement DBC?

There are different ways to implement DBC in your code, depending on the programming language and the tools you use. One common way is to use assertions, which are statements that check if a condition is true or false. If the condition is false, an exception is thrown, indicating that there is a bug or a violation of the contract. For example, in Java, you can use the assert keyword to write assertions, such as:

public class Account {
    private double balance; // invariant: balance must be non-negative
    public Account(double initialBalance) {
        assert initialBalance >= 0 : "Initial balance must be non-negative"; // precondition
        balance = initialBalance;
    }
    public void deposit(double amount) {
        assert amount > 0 : "Amount must be positive"; // precondition
        balance += amount;
        assert balance >= 0 : "Balance must be non-negative"; // invariant
    }
    public void withdraw(double amount) {
        assert amount > 0 : "Amount must be positive"; // precondition
        assert amount <= balance : "Amount must not exceed balance"; // precondition
        balance -= amount;
        assert balance >= 0 : "Balance must be non-negative"; // invariant
    }
    public double getBalance() {
        assert balance >= 0 : "Balance must be non-negative"; // invariant
        return balance; // postcondition: return the current balance
    }
}        

Another way to implement DBC is to use annotations, which are special markers that provide additional information about your code. Some languages, such as C# and Python, have built-in support for annotations, while others, such as Java, require external libraries or frameworks. For example, in Java, you can use the JContractor library to write annotations, such as:

import net.jcontractor.annotations.*;
@Invariant("balance >= 0")
public class Account {
    private double balance;
    @Pre("initialBalance >= 0")
    public Account(double initialBalance) {
        balance = initialBalance;
    }
    @Pre("amount > 0")
    @Post("balance == old(balance) + amount")
    public void deposit(double amount) {
        balance += amount;
    }
    @Pre("amount > 0 && amount <= balance")
    @Post("balance == old(balance) - amount")
    public void withdraw(double amount) {
        balance -= amount;
    }
    @Post("result == balance")
    public double getBalance() {
        return balance;
    }
}