Wie können Sie Ihren Code mit Design by Contract verifizieren?

1 Was ist DBC?

DBC basiert auf der Analogie eines Vertrags zwischen einem Lieferanten und einem Kunden, bei dem der Lieferant eine Dienstleistung oder ein Produkt bereitstellt und der Kunde es nutzt. Dieser Vertrag definiert die Verpflichtungen und Vorteile beider Parteien, wie z. B. die rechtzeitige und ordnungsgemäße Lieferung des Produkts durch den Lieferanten und die Zahlung des vereinbarten Preises durch den Kunden. Wenn eine der Parteien gegen den Vertrag verstößt, hat die andere Partei das Recht, die Beziehung zu beenden oder eine Entschädigung zu verlangen. Im objektorientierten Design besteht dieser Vertrag aus drei Elementen: Vorbedingungen, Nachbedingungen und Invarianten. Vorbedingungen sind Bedingungen, die vom Client erfüllt werden müssen, bevor eine Methode aufgerufen wird. Nachbedingungen sind Bedingungen, die der Lieferant nach der Rückkehr von einer Methode erfüllen muss; und Invarianten sind Bedingungen, die vom Lieferanten jederzeit eingehalten werden müssen. Durch das Definieren dieser Elemente können Sie Ihren Code besser verstehen, testen und wiederverwenden, indem Sie seine Verantwortlichkeiten und Annahmen angeben.

2 Wie implementiert man DBC?

Es gibt verschiedene Möglichkeiten, DBC in Ihrem Code zu implementieren, abhängig von der Programmiersprache und den Tools, die Sie verwenden. Eine gängige Methode ist die Verwendung von Assertionen, bei denen es sich um Anweisungen handelt, die überprüfen, ob eine Bedingung wahr oder falsch ist. Wenn die Bedingung false ist, wird eine Ausnahme ausgelöst, die angibt, dass ein Fehler oder ein Verstoß gegen den Vertrag vorliegt. In Java können Sie beispielsweise das Schlüsselwort assert verwenden, um Assertionen zu schreiben, z. B.:

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
    }
}        

Eine weitere Möglichkeit, DBC zu implementieren, ist die Verwendung von Anmerkungen, bei denen es sich um spezielle Markierungen handelt, die zusätzliche Informationen über Ihren Code bereitstellen. Einige Sprachen, wie z.B. C# und Python verfügen über eine integrierte Unterstützung für Annotationen, während andere, wie z. B. Java, externe Bibliotheken oder Frameworks erfordern. In Java können Sie beispielsweise die JContractor-Bibliothek verwenden, um Anmerkungen zu schreiben, z. B.:

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;
    }
}