Viele Experten halten Eiffel für die beste Programmiersprache, um wirklich zuverlässige Software zu entwickeln. Mit dem neuerdings freien Eiffelstudio stellen Sie diese Theorie auf den Prüfstand.

Design by Contract

Eines der zentralen Konzepte von Eiffel heißt Design by Contract. Der so genannte Vertrag (Contract) beschreibt die Zusammenarbeit der einzelnen Softwarekomponenten eines Systems mit Hilfe präziser Zusicherungen, also semantischer Bedingungen.

Wie im echten Leben hat auch beim Design by Contract der Anbieter Verpflichtungen gegenüber dem Kunden und umgekehrt. Nur sind eben in der Softwarewelt Anbieter und Kunden Softwarekomponenten. Vorteile von Design by Contract sind:

• Es hilft während der Implementation, weil die
  Zusicherungen gleichzeitig als Spezifikation der Software
  dienen.
• Verträge unterstützen die Entwicklung korrekter
  Software. Mit Design by Contract denkt der Programmierer über
  die Anforderungen jeder Routine nach und setzt diese in
  Programmcode um.
• Verträge dienen als Basis für die Dokumentation.
  Eiffelstudio zum Beispiel generiert die Dokumentation automatisch
  aus den Verträgen (»Project | Generate
  Documentation«).
• Mit Verträgen ist es einfacher, Fehler in einem Programm
  zu finden, weil die Ausführung an der Fehlerstelle stoppt.
  Autotest [10] erstellt aus den Verträgen automatisch
  Tests.

In Eiffel gibt es drei Hauptkategorien von Vertragsbedingungen: Klasseninvarianten (»invariant«), Vorbedingungen (»require«) und Nachbedingungen (»ensure«). Weitere Vertragsbedingungen sind Check-Instruktionen, Schleifeninvarianten und -varianten.

Bei allen Vertragsbedingungen bestehen die Zusicherungen aus einer Kennzeichnung (Tag) und einem booleschen Ausdruck der Form Kennzeichnung:Boolescher_Ausdruck. Das Tag ist optional, aber zur Dokumentation und zum Debuggen sehr nützlich.

Normalerweise prüft Eiffelstudio nur Vorbedingungen. Um auch die anderen Zusicherungen zu kontrollieren, müssen Sie sie unter »Project | Project Settings« und »Default assertions« aktivieren.

Klasseninvarianten müssen gelten, sobald eine Instanz der Klasse erzeugt ist und anschließend vor und nach der Ausführung von beliebigen Features der Klasse. Diese Regel gilt nur für qualifizierte Aufrufe der Form Objekt.Routine. Unqualifizierte Aufrufe der Form Routine und Aufrufe von nicht exportierten Features müssen die Klasseninvariante nicht bewahren. Die Klasse »HELLO« besitzt die Invariante, dass das Attribut »name« nie auf »Void« zeigen (Listing 1, Zeile 43) und nie leer sein darf (Zeile 44).

Bedingungen in Routinen

Vor- und Nachbedingungen kommen in Routinen zum Einsatz, die folgende Struktur besitzen:

name (argument_1: TYP_1; argument_2: TYP_2):RUECKGABE_TYP is
    -- Kommentar
  do
    ... -- Implementation
  end

Nach dem Namen der Routine steht in Klammern eine optionale Liste von Argumenten. Falls es sich bei der Routine um eine Funktion handelt, folgt nach einem Doppelpunkt der Typ des Rückgabewerts und schließlich das Schlüsselwort »is«. Der Kommentar einer Routine ist zwar optional, ihn einfach wegzulassen gilt aber in der Eiffel-Welt als äußerst schlechter Stil.

Die Implementation der Routine beginnt mit dem Schlüsselwort »do« und endet mit »end«. Startet sie mit »once« statt mit »do«, läuft die Routine während der Ausführung des Systems nur beim ersten Aufruf tatsächlich ab - unabhängig davon, wer der Aufrufer war. Spätere Aufrufe vom selben oder einem anderen Aufrufer zeigen keinen Effekt. Ist die Routine eine Funktion, gibt sie immer das Resultat zurück, das sie beim ersten Aufruf berechnet hat. Zudem gibt es noch die optionalen Blöcke »local«, »require« und »ensure«.

Die Zeile 12 von Listing 1 definiert die Routine »make«, die ohne Argumente und Rückgabewert auskommt. Die Prozedur ruft das Feature »set_name« mit einer Zeichenkette als Argument auf (Zeile 15). Die Routine »greeting« (Zeile 23) gibt einen »STRING« zurück. Die Spezialvariable »Result« referenziert den Rückgabewert einer Funktion. Handelt es sich dabei um einen erweiterten Typ, enthält »Result« direkt das Objekt.

»Result« wird beim Eintritt in die Funktion mit dem Standardwert des Rückgabetyps (Tabelle 1) initialisiert. Zeile 26 weist »Result« die Zusammensetzung aus »"Hello, "«, dem Rückgabewert der Query »name« und »"!"« zu. Die Syntax einer Zuweisung in Eiffel ist Variable := Wert. Das Gleichheitszeichen prüft, ob zwei Referenzen identisch sind.

Viele Experten halten Eiffel für die beste Programmiersprache, um wirklich zuverlässige Software zu entwickeln. Mit dem neuerdings freien Eiffelstudio stellen Sie diese Theorie auf den Prüfstand.