Eiffel-Befehle: Schnellreferenz für Design by Contract

Eiffel ist eine objektorientierte Programmiersprache von Bertrand Meyer, konzipiert 1985 und erstmals 1986 veröffentlicht (Eiffel Software). Ihr Markenzeichen ist Design by Contract: Software wird über explizit formulierte Verträge spezifiziert — Vorbedingungen, Nachbedingungen und Klasseninvarianten.

Klassen und Vererbung

• class ... end — Klassenrahmen
• feature — Abschnitt für Attribute und Routinen (Sichtbarkeit)
• inherit — Vererbung und Merkmals-Umbenennung
• create — Konstruktor-Routinen festlegen
• deferred / effective — abstrakte vs. konkrete Merkmale
• once — Routine nur einmal ausführen (Singleton-Muster)

Verträge und Schleifen

deposit (amount: INTEGER)
    require
        amount > 0
    do
        balance := balance + amount
    ensure
        balance = old balance + amount
invariant
    balance >= 0

• require — Vorbedingung der Routine
• ensure — Nachbedingung nach der Ausführung
• invariant — Klasseninvariante, gilt vor und nach jeder Routine
• old — Wert eines Ausdrucks vor der Routine
• loop ... invariant ... until ... variant ... end — Schleifen mit Vertrag

Weitere Elemente

local deklariert lokale Variablen, Result liefert den Rückgabewert einer Funktion, across iteriert über Container, attached prüft angehängte Referenzen und Void entspricht einer Null-Referenz. Entwicklungsumgebung ist EiffelStudio mit Compiler und der Klassenbibliothek EiffelBase.

Design by Contract hat viele Nachfolger gefunden — von Assertions über Contracts in .NET bis Ada. Verwandte Grundlagen: Objektorientierung und Smalltalk-Befehle.