Ada 2012: Neue Sprachversion verabschiedet
Seite 2: Contracts
Verträge und Typinvarianten
Neben den zahlreichen kleineren Änderungen sind es zwei große Features, die in diese Richtung gehen: Verträge und Typinvarianten. Anfang der 90er-Jahre führte Bertrand Meyer in seiner Programmiersprache Eiffel das Konzept des Vertrags (im Englischen Contract) ein. Der Vertrag einer Funktion besteht aus zwei booleschen Ausdrücken; die Vorbedingung drückt aus, was vor dem Aufruf der Funktion "wahr" sein muss, damit diese fehlerfrei arbeiten kann. Die Nachbedingung dagegen formuliert, was die Funktion ihrerseits bei der Rückkehr garantiert.
Der Begriff Vertrag kommt daher, dass diese booleschen Ausdrücke wie ein rechtlicher Vertrag Rechte und Pflichten beschreiben: Ist die Vorbedingung beim Aufruf der Funktion falsch, hat der Aufrufende die notwendigen Bedingungen nicht hergestellt. Ist die Nachbedingung falsch, muss der Entwickler den Fehler in der aufgerufenen Funktion suchen.
Meist übersetzt der Ada-Compiler die booleschen Ausdrücke intern als weitere Assertionen (Zusicherungen) am Anfang und am Ende der Funktion und erzeugt einen Programmabbruch mit informativer Fehlermeldung, wenn der boolesche Ausdruck falsch ist. In der Regel lassen sie sich aber, wie normale Assertionen, für den Produktionseinsatz abschalten.
Ein mit Verträgen verwandtes Konzept sind sogenannte Typinvarianten. Es handelt sich dabei ebenfalls um einen booleschen Ausdruck, diesmal gehört er aber zu einer Typ- oder Klassendefinition und beschreibt, welche zusätzlichen Eigenschaften sie besitzen soll. Wo Ada zusätzliche Assertionen einfügt, ist nicht so offensichtlich wie im Fall eines Vertrags Trotz ihrer Einfachheit hat niemand diese Konzepte in den Mainstream-Sprachen bis auf die Ausnahme Eiffel übernommen. Erst in den letzten Jahren gab es Forschungsprojekte, Verträge wenn nicht in die Sprachen selbst, so zumindest in die Tools einzubauen.
Aber was bringen Verträge? Schließlich muss der Programmierer mehr schreiben – zwei boolesche Ausdrücke pro Funktion. Erstens gehören Verträge wie die Parametertypen zum Interface einer Funktion. Ein API-Client kann an den Verträgen direkt ablesen, wie er eine Funktion verwenden soll und was sie garantiert. Zweitens wirken Verträge wie zusätzliche Assertionen und können in der Entwicklungsphase nützlich sein. Vor allem aber sind sie ein erster Schritt hin zur Softwareverifikation. So lassen sich Verträge zur manuellen oder automatischen Erzeugung von Unit-Tests heranziehen. Der Unit-Test einer Funktion, der die Vorbedingung der Funktion nicht erfüllt, ergibt zum Beispiel keinen Sinn. Verträge sind zudem nützliche Mehrinformationen für eine statische Analyse des Codes. Im besten Fall lässt sich sogar beweisen, dass die Funktion keinen Laufzeitfehler verursachen kann und ihren Vertrag erfüllt.
Verdeutlichen lässt sich das anhand des Beispiels im Codebeispiel oben. Hier wurde zu jeder Funktion eine Vor- und Nachbedingung hinzugefügt. Die Prozedur Push erkennt man im zweiten hervorgehobenen Teil. Die Vor- und Nachbedingung, definiert durch die Aspekte Pre und Post, sind einfach boolesche Ausdrücke. Die Vorbedingung sagt, dass vor dem Push der Puffer nicht voll sein sollte. Die Nachbedingung garantiert, dass danach der Puffer nicht leer ist (er enthält ja mindestens das gerade hinten angefügte Element) und dass die Länge des Puffers, also die Anzahl der gespeicherten Elemente, um eins erhöht wurde.
Es bleiben die Typinvarianten, zu sehen im ersten im Code hervorgehobenen Teil. Hier wird nicht nur der Wertebereich des Integer-Typen beschränkt, sondern auch festgelegt, dass nur gerade Zahlen zu diesem Typen gehören. Das erreicht man mit der Syntax Dynamic_Predicate => und dem nachfolgendem booleschen Ausdruck. Er wird immer ausgeführt, wenn das Programm einer Variablen dieses Typs einen neuen Wert zuweist oder eine Variable eines anderen Typs (zum Beispiel Integer) in diesen Typ konvertiert. Im Prinzip sind demnach nur gerade Zahlen Vertreter des Typs Content. Ein Aufruf von Push (S, 3); bricht mit einer Fehlermeldung ab, während Push (S, 2); erfolgreich ist.
Es gibt noch andere Formen von Typinvarianten in Ada 2012. Genauer gesagt hat das Standardisierungskomitee die gezeigte Form als „Subtype predicate“ bezeichnet, während der Begriff "Type Invariant" für die Variante reserviert ist, bei der das Prädikat nur bei bestimmten Funktionsaufrufen überprüft wird. Der Begriff "Typinvariante" ist jedoch für beide Varianten gebräuchlich. Ein gut dokumentiertes Programm, das keine Verträge benutzt, würde die entsprechenden Informationen vermutlich trotzdem enthalten, aber in der Form von Kommentaren. Diese sind prinzipiell wünschenswert, wenn sie korrekt sind und mit den Evolutionen der Software mitgehen. Formal definierte Sprachelemente wie Verträge sind aber wirksamer, da diese Informationen nun auch den Werkzeugen zur Verfügung stehen. Dadurch hat der Programmierer der API daran Interesse, die Informationen auf dem neuesten Stand zu halten.
Im Beispielprogramm gibt es trotzdem noch Kommentare, und das ist auch gut so. Hierbei handelt es sich einerseits um Erklärungen, die streng genommen nicht notwendig, aber nützlich für den API-Client sind, und andererseits um nicht mit Verträgen und Invarianten ausgedrückte Eigenschaften. Insbesondere die FIFO-Semantik (First In, First Out) des Puffers wird nicht formell beschrieben. Sie ließe sich auch mit Verträgen beschreiben. Solche komplexeren Verträge sind vor allem von Nutzen, wenn sich formale Analysemethoden auf das Programm anwenden lassen, und erhöhen nicht unbedingt die Lesbarkeit.
Weitere Neuerungen kurz und knapp
Die Verträge werden in Ada 2012 durch sogenannte Aspekte der Funktion oder der Prozedur beigefügt. In der Nachbedingung (im Aspekt Post) lassen sich spezielle Attribute verwenden. F'Result steht für das Ergebnis des Funktionsaufrufs von F, während X'Old für den Wert von X vor dem Aufruf der Funktion steht. Die folgende Prozedur inkrementiert ihr Argument:
procedure Incr (X : in out Integer)
with Pre => (X < Integer'Last),
Post => (X = X'Old + 1);
Eher kosmetischer Natur, aber praktisch sind die sogenannten Ausdrucksfunktionen: Das sind solche, deren Resultat nicht durch eine Sequenz von Statements, sondern durch einen einzigen Ausdruck definiert ist. Sie haben eine bequemere Syntax und können, im Unterschied zu herkömmlichen Funktionen, auch in Spezifikationen von Paketen auftreten:
function Expr_Fun (X : Integer) return Integer is (X + 1);
Vergleichbar mit dem im Artikel erwähnten Untertyp-Prädikat sind die Typinvarianten, die ein Programmierer nur für sogenannte private Typen definieren kann, die Teil einer Paket-Schnittstelle sind:
type T is private
with Type_Invariant => (Is_Valid (T));
Wenn nun eine Funktion dieser Paket-Schnittstelle aufgerufen wird, wird der boolesche Ausdruck für alle Parameter vom Typ T sowie für den Rückgabewert, falls er auch vom Typ T ist, am Ende der Funktion überprüft.
Fazit
Mit Ada 2012 bringen die Sprachdesigner ein paar brauchbare Konzepte aus der Forschung in den Mainstream. Sie haben durchaus das Potenzial, die Wartbarkeit und Verifizierbarkeit von Software zu erhöhen. Die Arbeit an Ada 2012 war seit Frühjahr 2012 abgeschlossen; nun hat die ISO-Organisation die neue Sprachversion abgesegnet. Der kostenlose und quelloffene Ada-Compiler GNAT GPL der Firma AdaCore unterstützt Ada 2012 übrigens bereits vollständig.
Johannes Kanig
ist Software Engineer bei AdaCore in Paris.
Literatur
(ane)
