Mehr Sicherheit in der Programmierung Ada für Embedded

Reiches Typsystem ist gerade im Embedded-Bereich nützlich

Die einfachste Art und Weise, in Ada eine Funktionsdeklaration zu bereichern, ist, zu deklarieren, wie die Parameter einer Funktion verwendet werden. Ein Beispiel:

function F (A : in Integer; B : out Integer; C : in out Integer) return Integer;

Hier wurde deklariert, dass die Funktion F die Variable A nur liest, aber nicht schreibt (»in«), die Variable B nur schreibt, aber nicht liest (»out«), und schließlich die Variable C liest und schreibt (»in out«). Für solche Deklarationen muss man in C schon Zeiger verwenden; in Ada reichen diese einfachen Annotationen.

Eine weitere Art, eine Funktionsdeklaration anzureichern, ist, die Typen der Argumente und des Rückgabewerts genauer zu definieren; zum Beispiel:

type Temperature is range -55 .. 125; function Read_Temperature (This : Sensor) return Temperature;

Hier wurde, statt die Temperatur einfach als Integer darzustellen, ein deutlich präziserer Datentyp gewählt, der zum Beispiel den Wertebereich der Daten beschreibt, die laut Spezifikation vom Sensor tatsächlich ausgelesen werden können. Diese genaue Spezifikation befreit Benutzer dieser Funktion, die Rückgabe von ungültigen Werten zu überprüfen und zu reagieren. Falls der Sensor einen anderen Wert zurückgibt, wird das vom Programm per Check zur Laufzeit entdeckt, und man kann auf einen Material- oder Spezifikationsfehler schließen.

Im nächsten Beispiel erwartet eine Funktion eine Liste (implementiert als Zeiger) als Argument, doch die Liste soll schon angelegt sein (der Zeiger soll nicht null sein). Das kann man in Ada so schreiben:

function Is_Empty (List : not null access My_List) return Boolean;

Das Schlüsselwort »access« ist Ada-Syntax für Zeiger, und »not null« deklariert, dass hier ein Null-Zeiger nicht erwünscht ist.

Das mächtigste Sprachkonstrukt der vertragsbasierten Programmierung sind jedoch die Vor- und Nachbedingungen, bzw. der pre- und postconditions. Diese sind zwei boolesche Ausdrücke, die man einer Funktion hinzufügt, wobei auch nur einer von beiden angegeben werden kann. Die Vorbedingung (pre) soll direkt vor dem Aufruf der Funktion wahr sein, die Nachbedingung (post) soll bei der Rückgabe des Resultats gültig sein. Diese Ausdrücke können wie Assertionen zur Laufzeit ausgeführt werden. Ein Beispiel einer typischen API soll hier genügen. Der API-Benutzer soll vor dem Auslesen des Sensors diesen initialisieren, mit einem Aufruf der Funktion Initialize:

type Sensor is private;

function Initialized (This : Sensor) return Boolean;

procedure Initialize (This : in out Sensor) with Post => Initialized (This);

function Read_Temperature (This : Sensor) return Temperature

with Pre => Initialized (This);

Zuerst wird eine Hilfsfunktion Initialized definiert, die dann später in den Pre- und Postausdrücken verwendet wird. Die Funktion »Read_Temperature« hat die Vorbedingung, dass der Sensor initialisiert sein soll; ausgedrückt durch die Hilfsfunktion. Diese Eigenschaft kann durch einen Aufruf der Initialize-Funktion erreicht werden.

Verträge spielen in SPARK, einer Sprache, die von Ada ausgeht und die einige gefährliche Sprachfeatures wie Zeiger komplett ausschließt, eine noch größere Rolle. Sie erlauben es, die völlige Abwesenheit von Laufzeitfehlern – wie Buffer overflows oder Division durch null – mathematisch zu beweisen, und auch die Gültigkeit der Pre- und Postconditions selbst restlos zu beweisen.

Diese vorgestellten Features der Programmiersprache Ada können in der eingebetteten Programmierung den Unterschied machen. Das reiche Typsystem, das dank der Repräsentationsklauseln auch in der Low-Level-Programmierung verwendet werden kann, sowie moderne Features wie die objektorientierte und vertragsbasierte Programmierung sind gerade im Embedded-Bereich nützlich.