Der Reiz der Sprache Ada — Design in Typen ausdrücken und Software, die jahrzehntelang läuft
· Go Komura · Ada, Programmiersprache, Starke Typisierung, SPARK, GNAT, Alire, Hohe Integrität, Embedded, Hohe Zuverlässigkeit
1. Zuerst das Wichtigste
Haben Sie schon einmal von einer Sprache namens Ada gehört?
Viele haben vielleicht den Eindruck „eine alte Sprache“, „eine Sprache fürs Militär“ oder „der Name kam nur mal im Unterricht vor“.
Doch Ada ist auch heute noch eine aktive Sprache.
In der Welt der Software, bei der ein Stillstand Menschenleben gefährdet — Flugsteuerungen von Flugzeugen, Signalsysteme der Eisenbahn, Raketen, Flugsicherung, Satelliten, Medizingeräte —, wird Ada seit Jahrzehnten eingesetzt.
Beim Verständnis von Ada ist die folgende Sichtweise wichtig.
Ada ist eine Sprache, die alles darauf ausrichtet, Fehler vor der Ausführung auszumerzen
Typen sind kein Behälter für Daten, sondern ein Werkzeug, um die Designabsicht auszudrücken
Die Trennung von Spezifikation und Implementierung, Verträge und Nebenläufigkeit sind in die Sprache integriert
Die Sprache wurde nicht zum Trend, aber ihre Designphilosophie lebt in modernen Sprachen fort
In diesem Artikel werden die Geschichte, die Syntax, die starke Typisierung, die Bereichsbeschränkungen, die Pakete, das Design by Contract, die Tasks, SPARK, die Entwicklungsumgebung und schließlich auch die Schwächen von Ada besprochen — der Reiz von Ada wird zusammengefasst.
Das Ziel ist, dass Leserinnen und Leser, die üblicherweise C#, C++ oder Java schreiben, das Gefühl mitnehmen, „Design in Typen auszudrücken“.
Da es insgesamt 21 lange Kapitel sind, hier zuerst eine Übersicht.
Aufbau dieses Artikels:
Kapitel 1–3 Was Ada ist, seine Geschichte und wo es eingesetzt wird
Kapitel 4–5 Der erste Schritt (Hello, World) und eine auf Lesbarkeit ausgelegte Syntax
Kapitel 6–11 Das Typsystem: starke Typisierung, Bereichsbeschränkungen, Arrays, Pakete, Records, Generics
Kapitel 12–13 Ausnahmebehandlung und Design by Contract (Pre/Post)
Kapitel 14–15 Nebenläufigkeit: Tasks und geschützte Objekte
Kapitel 16–17 Formale Verifikation mit SPARK und Interoperabilität mit C/C++
Kapitel 18 Entwicklungsumgebung (GNAT und Alire)
Kapitel 19–21 Schwächen und Vorbehalte, der Wert aus Sicht langlebiger Software, Zusammenfassung
Wer sofort etwas zum Laufen bringen möchte, kann direkt zu Kapitel 4 und 18 springen, und wer nur die Designphilosophie erfassen möchte, kann sich auf die Kapitel 1, 6, 7 und 13 beschränken — der Artikel ist so geschrieben, dass auch selektives Lesen funktioniert.
Die in diesem Artikel vorkommenden Codeausschnitte sind als Referenzsammlung, nach Kapiteln in Dateien geordnet, auf GitHub veröffentlicht.
ada-language-appeal - komurasoft-blog-samples (GitHub)
2. Was ist Ada? — Namensherkunft und Geschichte
Ada ist eine allgemeine Programmiersprache, die in der zweiten Hälfte der 1970er-Jahre unter Federführung des US-Verteidigungsministeriums (DoD) entstand.
Das Verteidigungsministerium hatte damals ein Problem: In jedem Projekt wurde eine andere Sprache verwendet, wodurch die Wartungskosten der Software explodierten.
Daher wurde in einem internationalen Design-Wettbewerb eine Standardsprache ausgewählt, die sich auch für eingebettete Systeme und Echtzeitsysteme eignet.
Den Zuschlag erhielt der Entwurf des von Jean Ichbiah geleiteten Teams.
Der Sprachname Ada geht auf Ada Lovelace zurück (Augusta Ada King, Countess of Lovelace), die oft als die erste Programmiererin der Welt bezeichnet wird.
Grob zusammengefasst sieht die Geschichte von Ada so aus.
1980 Die erste Spezifikation wird als MIL-STD-1815 festgelegt
1983 Ada 83 (ANSI-Standard)
1987 Wird ISO-Standard
1995 Ada 95 (Einführung von Objektorientierung und geschützten Objekten)
2005 Ada 2005 (Interfaces, erweiterte Containerbibliothek)
2012 Ada 2012 (Design by Contract als Sprachfeature eingeführt)
2022 Ada 2022 (aktueller Standard)
Ada 95 war eine der allerersten ISO-standardisierten objektorientierten Sprachen.
Und mit Ada 2012 wurde Design by Contract — Vorbedingungen, Nachbedingungen und Typinvarianten — in die Sprachspezifikation aufgenommen.
Ada ist keine „alte Sprache“, sondern eine Sprache, die seit über 40 Jahren fortlaufend weiterentwickelt wird.
3. Wo Ada eingesetzt wird
Der klassische Bereich, in dem Ada nach wie vor eingesetzt wird, sind Systeme, die hohe Verlässlichkeit (High Integrity) erfordern.
Flugsteuerung und Avionik ziviler Flugzeuge
Flugsicherungssysteme
Signal- und Sicherungssysteme der Eisenbahn
Raketen und Satelliten
Verteidigungssysteme
Medizingeräte
Teile der Kernsysteme im Finanz- und Industriebereich
Diese Bereiche haben gemeinsame Merkmale.
Fehler wirken sich unmittelbar auf Menschenleben oder enorme Verluste aus
Zertifizierung und Audits verlangen einen Nachweis der Korrektheit
Ist ein System einmal ausgerollt, läuft es Jahrzehnte weiter
Nachträgliche Korrekturen sind extrem teuer
Es ist eine Welt, in der der Gedanke „nach dem Release reparieren wir es einfach“ nicht funktioniert.
Das Sprachdesign von Ada ist genau darauf ausgerichtet, diesen Anforderungen zu begegnen.
Fehler, die zur Compile-Zeit erkennbar sind, werden zur Compile-Zeit erkannt; was sich nur zur Laufzeit feststellen lässt, wird durch Laufzeitprüfungen abgefangen; und darüber hinaus gilt: Was sich mathematisch beweisen lässt, wird durch Beweis ausgemerzt — dieser Gedanke durchzieht die gesamte Sprache.
Dieser Gedanke lohnt sich auch für Entwicklerinnen und Entwickler, die Web- oder Desktop-Businessanwendungen schreiben.
4. Zuerst Hello, World
Werfen wir einen Blick auf Ada-Code.
with Ada.Text_IO;
procedure Hello is
begin
Ada.Text_IO.Put_Line ("Hello, Ada!");
end Hello;
Dieser Code lässt sich speichern und sofort ausführen. Der gängigste Ada-Compiler ist GNAT (der in GCC enthaltene, kostenlose Ada-Compiler; auch die Compileroptionen der Codebeispiele in diesem Artikel beziehen sich auf GNAT), und Build und Ausführung benötigen zwei Zeilen.
gnatmake hello.adb -> erzeugt die ausführbare Datei hello (unter Windows hello.exe)
./hello -> Hello, Ada!
Der Dateiname folgt der Regel „Unit-Name in Kleinbuchstaben + .adb“ (für procedure Hello also hello.adb). Wie Sie GNAT selbst bekommen und wie es mit dem Paketmanager Alire noch etwas bequemer geht, ist in Kapitel 18 zusammengefasst. Wer zuerst die Umgebung einrichten und direkt loslegen möchte, kann jetzt gleich zu Kapitel 18 springen.
Das Erste, was vermutlich auffällt, sind folgende Punkte.
with bindet eine Bibliothekseinheit ein
Der Programmkörper ist eine Prozedur (procedure)
begin / end umschließen einen Block
Nach end wird der Name wiederholt
Anweisungen enden mit einem Semikolon
Dass am Ende der Name noch einmal ausgeschrieben wird, wie in end Hello;, ist typisch für Ada.
Selbst wenn Blöcke tief verschachtelt sind, ist auf einen Blick erkennbar, „wozu dieses end gehört“.
Der Compiler prüft außerdem, ob die Namen zusammenpassen, sodass ein falsch geschlossener Block zu einem Compile-Fehler wird.
Das wirkt wie eine Kleinigkeit, zeigt aber gut die Philosophie von Ada: Die Sprache unterstützt den Menschen genau dort, wo Lesefehler leicht passieren.
5. Auf Lesbarkeit ausgelegte Syntax
Adas Syntax ist so gestaltet, dass sie Lesbarkeit über Schreibbarkeit stellt.
Denn sie geht von der Prämisse aus, dass Software weit häufiger gelesen als geschrieben wird.
Schleifen und Verzweigungen werden zum Beispiel so geschrieben.
for I in 1 .. 5 loop
Ada.Text_IO.Put_Line (Integer'Image (I * I));
end loop;
if Temperature > 80.0 then
Start_Cooling;
elsif Temperature < 20.0 then
Start_Heating;
else
Keep_Current_State;
end if;
Die case-Anweisung hat eine typisch Ada-hafte Eigenschaft.
case Today is
when Mon .. Fri =>
Put_Line ("Weekday");
when Sat | Sun =>
Put_Line ("Weekend");
end case;
Die Punkte sind:
Ein case muss alle Werte abdecken, sonst ist es ein Compile-Fehler
Es gibt kein implizites Durchfallen wie in C-artigen Sprachen
Bedingungen lassen sich über Bereiche (Mon .. Fri) und Alternativen (Sat | Sun) bündeln
Fügt man einem Aufzählungstyp einen Wert hinzu, wird jede nicht vollständige case-Anweisung zu einem Compile-Fehler.
Die Erfahrung, dass „der Compiler die von einer Spezifikationsänderung betroffenen Stellen auflistet“, lässt einen nicht mehr los, sobald man sie einmal gemacht hat.
Auch Argumente lassen sich namensbasiert zuordnen.
Draw_Rectangle (Left => 10, Top => 20, Width => 100, Height => 50);
Das verhindert eine Verwechslung von Argumenten, und der aufrufende Code wird selbst zur Dokumentation.
Zuweisung ist :=, Vergleich ist =, sodass eine Verwechslung wie beim if (a = b) C-artiger Sprachen bereits auf syntaktischer Ebene nicht auftreten kann.
6. Starke Typisierung — Einheitenverwechslungen zu Compile-Fehlern machen
Adas größter Reiz ist seine starke Typisierung.
In vielen Sprachen wird der Begriff „stark typisiert“ verwendet, aber bei Ada geht das noch eine Stufe tiefer.
In Ada sind Typen, die unter unterschiedlichen Namen deklariert wurden, verschiedene Typen — selbst wenn ihre Struktur völlig identisch ist.
type Meters is new Float;
type Seconds is new Float;
Distance : Meters := 100.0;
Time : Seconds := 9.58;
Beide sind im Kern Fließkommazahlen, lassen sich aber nicht vermischen.
Distance := Time; -- Compile-Fehler
Distance := Distance + Time; -- Compile-Fehler
Nur wenn absichtlich umgewandelt werden soll, wird das explizit geschrieben.
Speed : constant Float := Float (Distance) / Float (Time);
Warum diese Strenge?
Nicht wenige reale Softwareunfälle gehen auf „Einheitenverwechslungen“ zurück.
Ein bekanntes Beispiel: Die Marssonde Mars Climate Orbiter ging 1999 verloren, weil imperiale und metrische Einheiten vermischt wurden.
Adas Antwort ist einfach.
Meter und Fuß zu unterschiedlichen Typen machen
Eine Vermischung zu einem Compile-Fehler machen
Umwandlungen explizit erzwingen
Nicht „vorsichtig sein“, nicht „im Review entdecken“, nicht „im Test abfangen“, sondern den Build von vornherein nicht durchlaufen lassen.
Das ist Adas Grundhaltung.
7. Bereichsbeschränkungen — ungültige Werte bereits auf Datentypebene verhindern
In Ada kann ein Typ einen Wertebereich mitführen.
subtype Percentage is Integer range 0 .. 100;
Progress : Percentage := 50;
Der Versuch, einer Variablen vom Typ Percentage einen Wert außerhalb dieses Bereichs zuzuweisen, löst zur Laufzeit die Ausnahme Constraint_Error aus.
Progress := 120; -- Zur Laufzeit Constraint_Error
Verstöße, die sich zur Compile-Zeit erkennen lassen, werden zur Compile-Zeit erkannt.
Implizite Annahmen wie „dieser Wert sollte zwischen 0 und 100 liegen“ oder „dieser Wert sollte mindestens 1 sein“ lassen sich so nicht in einem Kommentar, sondern im Typ selbst ausdrücken.
Tatsächlich sind in Adas Standardbibliothek bereits häufig verwendete beschränkte Typen vordefiniert.
Natural = Integer range 0 .. Integer'Last
Positive = Integer range 1 .. Integer'Last
Seit Ada 2012 lassen sich außerdem beliebige Bedingungen als Prädikate anhängen.
subtype Even is Integer
with Dynamic_Predicate => Even mod 2 = 0;
Auch Typen für die Hardwaresteuerung, etwa Festkommatypen, sind in die Sprache integriert.
type Temperature is delta 0.1 range -50.0 .. 150.0;
In vielen Sprachen läuft die Prüfung auf ungültige Werte tendenziell so ab.
Validierung per if-Anweisung am Anfang der Funktion
Fehlende Prüfungen sind Sache des Code-Reviews
Unklar, welche Funktionen bereits geprüfte Werte erhalten
In Ada lässt sich sagen: „Allein weil ein Wert diesen Typ hat, ist der Bereich bereits garantiert.“
Weil die Verantwortung für die Validierung in den Datentyp verlagert wird, kann sich die Funktionslogik auf ihre eigentliche Aufgabe konzentrieren.
8. Arrays und Indizes — Grenzprüfung und Indizierung über Aufzählungstypen
Bei Ada-Arrays lässt sich der Typ des Indexes frei wählen.
type Day is (Mon, Tue, Wed, Thu, Fri, Sat, Sun);
type Hours_Array is array (Day) of Natural;
Work_Hours : Hours_Array := (Mon .. Fri => 8, others => 0);
Das ist ein Array, das über den Aufzählungstyp Day indiziert wird.
Der Zugriff erfolgt als Work_Hours (Wed), ohne sich merken zu müssen, „wofür dieser numerische Index steht“.
Auch Schleifen lassen sich entlang des Indextyps schreiben.
for D in Work_Hours'Range loop
Put_Line (Day'Image (D) & ":" & Natural'Image (Work_Hours (D)));
end loop;
Mit Attributen wie 'Range, 'First, 'Last und 'Length lassen sich die Grenzen eines Arrays jederzeit abrufen.
Weil die Grenzen nicht fest codiert sind, wirkt sich eine Größenänderung des Arrays nicht auf die Schleifen aus.
Und entscheidend ist: Array-Zugriffe werden immer auf ihre Grenzen geprüft.
Buffer : String (1 .. 10);
Index : Integer := 11;
Buffer (Index) := 'x'; -- Zur Laufzeit Constraint_Error
Pufferüberläufe in C/C++ sind seit Jahrzehnten eine der Hauptursachen für Sicherheitslücken.
In Ada ist ein Zugriff außerhalb der Grenzen kein undefiniertes Verhalten, sondern eine definierte Ausnahme.
Statt den Speicher lautlos zu beschädigen und irgendwo anders einen mysteriösen Absturz zu verursachen, hält das Programm sofort und mit lautem Knall genau an der Stelle an, an der das Problem entsteht.
Angesichts der Untersuchungskosten bei langfristig betriebenen Systemen ist dieser Unterschied enorm.
9. Pakete — Trennung von Spezifikation und Implementierung
Adas Modulmechanismus ist das Paket (package).
Ein Paket teilt sich in zwei Dateien auf: die Spezifikation (spec) und den Rumpf (body).
counters.ads Spezifikation: die nach außen freigegebene Schnittstelle
counters.adb Rumpf: die Implementierungsdetails
Die Spezifikation wird so geschrieben.
package Counters is
type Counter is private;
procedure Increment (C : in out Counter);
function Value (C : Counter) return Natural;
private
type Counter is record
Count : Natural := 0;
end record;
end Counters;
Der Rumpf wird so geschrieben.
package body Counters is
procedure Increment (C : in out Counter) is
begin
C.Count := C.Count + 1;
end Increment;
function Value (C : Counter) return Natural is
begin
return C.Count;
end Value;
end Counters;
Beachtenswert sind folgende Punkte.
Wird ein type als private deklariert, kommt die nutzende Seite nicht an die interne Struktur heran
Allein das Lesen der Spezifikation (.ads) genügt, um die Verwendung vollständig zu verstehen
Änderungen am Rumpf (.adb) erfordern, solange die Spezifikation gleich bleibt, nur minimale Neukompilierung auf Nutzerseite
Das ähnelt C/C++-Headerdateien, aber statt einer textuellen Expansion wie bei #include wird die Konsistenz als Teil der Sprachspezifikation geprüft.
Eine Abweichung zwischen Spezifikation und Rumpf ist ein Compile-Fehler.
Außerdem muss jedem Parameter zwingend ein Modus mitgegeben werden: in, out oder in out.
procedure Increment (C : in out Counter);
Ob ein Parameter nur gelesen, nur geschrieben oder gelesen und geschrieben wird, ist allein an der Signatur erkennbar.
Selbst ohne Kenntnis von Zeigern oder Referenzen lässt sich die Richtung des Datenflusses ablesen.
10. Records und Diskriminanten
Das Ada-Gegenstück zu einem Struct ist der Record.
type Point is record
X : Float := 0.0;
Y : Float := 0.0;
end record;
P : Point := (X => 1.0, Y => 2.0);
Felder können Standardwerte tragen, und über Aggregate ist eine namensbasierte Initialisierung möglich.
Ein typisches Ada-Feature ist der Diskriminant (discriminant).
type Buffer (Size : Positive) is record
Data : String (1 .. Size);
Length : Natural := 0;
end record;
Small : Buffer (Size => 16);
Large : Buffer (Size => 4096);
Ein Diskriminant ist ein Parameter, der die „Form“ eines Records festlegt.
Buffer (16) und Buffer (4096) sind vom selben Typ, aber die Größe des internen Arrays wird bei der Deklaration festgelegt und ändert sich danach nicht mehr.
Man kann sich das vorstellen wie das, was man in C als „Struct mit variabel langem Member plus Größenfeld“ bezeichnen würde — nur dass die Sprache dies sicher als Typ verwaltet.
Die in C übliche Fehlerquelle, dass Größe und tatsächlicher Inhalt nicht mehr zusammenpassen, existiert von vornherein nicht.
11. Generics
Ada besitzt bereits seit seinem ersten Standard von 1983 Generics.
Das ist deutlich früher als C++-Templates (1990er-Jahre) oder Java-Generics (2004).
generic
type Element is private;
procedure Swap (Left, Right : in out Element);
procedure Swap (Left, Right : in out Element) is
Temp : constant Element := Left;
begin
Left := Right;
Right := Temp;
end Swap;
Die nutzende Seite instanziiert mit konkreten Typen.
procedure Swap_Integers is new Swap (Element => Integer);
procedure Swap_Floats is new Swap (Element => Float);
Das charakteristische Merkmal von Adas Generics ist, dass die geforderten Operationen explizit angegeben werden.
generic
type Element is private;
with function "<" (Left, Right : Element) return Boolean is <>;
function Max (Left, Right : Element) return Element;
In der Spezifikation steht: „Diese generische Funktion verlangt vom Typ Element einen Vergleichsoperator.“
Das Problem, unter dem C++-Templates lange gelitten haben — dass ein Fehler erst bei der Instanziierung sichtbar wird —, tritt in Ada von vornherein nicht auf.
Das Problem, das C++20-Concepts und Rusts Trait-Bounds zu lösen versuchten, hatte Ada bereits vor 40 Jahren beantwortet.
12. Ausnahmebehandlung
Ada verfügt über eine Ausnahmebehandlung.
with Ada.Text_IO;
with Ada.Exceptions;
procedure Read_Config is
begin
Load_File ("config.txt");
exception
when Ada.Text_IO.Name_Error =>
Ada.Text_IO.Put_Line ("Konfigurationsdatei nicht gefunden");
when E : others =>
Ada.Text_IO.Put_Line (Ada.Exceptions.Exception_Information (E));
raise;
end Read_Config;
Am Ende eines Blocks wird ein exception-Teil geschrieben, in dem für jede Art von Ausnahme ein Handler aufgeführt wird.
Zu den sprachdefinierten Ausnahmen gehören unter anderem folgende.
Constraint_Error Verstoß gegen Bereichsbeschränkungen, Array-Grenzverletzung, Division durch Null usw.
Program_Error Verstoß gegen Sprachregeln (z. B. das Erreichen einer Stelle, die nie erreicht werden darf)
Storage_Error Speichermangel
Tasking_Error Fehlschlag der Kommunikation zwischen Tasks
Bemerkenswert ist, dass Verstöße gegen Bereichsbeschränkungen und Grenzprüfungen vollständig in diesen Ausnahmemechanismus integriert sind.
Wird eine „im Typ festgelegte Beschränkung“ verletzt, entsteht ein Constraint_Error.
Mit anderen Worten: Die in Kapitel 7 gesehenen Bereichsbeschränkungen fungieren als automatisch generierte Laufzeit-Assertions.
Es besteht keine Notwendigkeit, selbst überall Prüfcode in Form von if-Anweisungen zu verstreuen.
13. Design by Contract — Pre-/Post-Bedingungen als Sprachfeature
Das Highlight von Ada 2012 ist die Sprachunterstützung für Design by Contract.
Vorbedingungen (Pre) und Nachbedingungen (Post) lassen sich direkt an Unterprogrammen angeben.
package Stacks is
type Stack is private;
function Is_Full (S : Stack) return Boolean;
function Is_Empty (S : Stack) return Boolean;
function Count (S : Stack) return Natural;
procedure Push (S : in out Stack; Item : Integer)
with Pre => not Is_Full (S),
Post => Count (S) = Count (S)'Old + 1;
procedure Pop (S : in out Stack; Item : out Integer)
with Pre => not Is_Empty (S),
Post => Count (S) = Count (S)'Old - 1;
private
-- Implementierungsdetails
end Stacks;
Pre ist „das Versprechen, das die aufrufende Seite einhalten muss“, Post ist „das Versprechen, das die Implementierung garantiert“.
Mit dem Attribut 'Old lässt sich der Wert vor dem Aufruf referenzieren.
Dieser Vertrag lässt sich über eine Compileroption (-gnata bei GNAT) als Laufzeitprüfung aktivieren.
Bei einem Vertragsverstoß wird eine Assertion_Error-Ausnahme ausgelöst, und welche Seite das Versprechen gebrochen hat, wird eindeutig.
Pre-Verstoß -> Fehler auf der aufrufenden Seite
Post-Verstoß -> Fehler in der Implementierung
Worin unterscheidet sich das von einem Dokumentationskommentar wie „Diese Funktion darf nicht mit einem leeren Stack aufgerufen werden“?
Ein Kommentar kann von der Implementierung abweichen, ohne dass es jemand bemerkt
Ein Vertrag wird vom Compiler auf Syntax und Typen geprüft
Ein Vertrag lässt sich automatisch zur Laufzeit verifizieren
Ein Vertrag wird zur Eingabe für den statischen Beweis mit SPARK (Kapitel 16)
Die Spezifikation existiert in überprüfbarer Form direkt im Code.
Das ist die Welt von Ada 2012 und danach.
Mit Typinvarianten (Type_Invariant) lassen sich auch Beschränkungen der Form „Werte dieses Typs erfüllen stets diese Eigenschaft“ ausdrücken.
14. Tasks — Nebenläufigkeit ist in die Sprache integriert
Ein weiterer großer Reiz von Ada ist, dass Nebenläufigkeit Teil der Sprachspezifikation ist.
Während C/C++ für Threads auf Betriebssystem-APIs oder Bibliotheken (pthread, std::thread) angewiesen sind, hatte Ada Tasks bereits 1983 in die Sprache integriert.
with Ada.Text_IO;
procedure Task_Demo is
task Worker;
task body Worker is
begin
for I in 1 .. 3 loop
Ada.Text_IO.Put_Line ("worker:" & Integer'Image (I));
delay 0.5;
end loop;
end Worker;
begin
for I in 1 .. 3 loop
Ada.Text_IO.Put_Line ("main :" & Integer'Image (I));
delay 0.5;
end loop;
end Task_Demo;
Wird ein task deklariert, beginnt die parallele Ausführung in dem Moment, in dem der umschließende Block startet.
Und entscheidend ist: Der Block endet erst, wenn alle darin enthaltenen Tasks beendet sind.
Fehler der Art „das Joinen eines Threads vergessen, wodurch beim Prozessende seltsame Dinge passieren“ können strukturell nicht auftreten.
Für die Synchronisation zwischen Tasks gibt es das Sprachfeature Rendezvous.
task Logger is
entry Write (Message : String);
end Logger;
task body Logger is
begin
loop
select
accept Write (Message : String) do
Ada.Text_IO.Put_Line (Message);
end Write;
or
terminate;
end select;
end loop;
end Logger;
Die nutzende Seite schreibt Logger.Write ("hello"); — in derselben Form wie einen Prozeduraufruf.
Kommunikation zwischen Tasks über Nachrichtenübermittlung lässt sich schreiben, ohne irgendetwas über Locks zu wissen.
Für Echtzeitsysteme sind sogar Schedulingstrategien, die Kontrolle von Prioritäten und, für bessere Verifizierbarkeit, das die Tasking-Funktionen einschränkende Ravenscar-Profil standardisiert.
15. Geschützte Objekte — wechselseitigen Ausschluss als Typ schreiben
Für den wechselseitigen Ausschluss bei gemeinsam genutzten Daten wird das in Ada 95 eingeführte geschützte Objekt (protected object) verwendet.
protected Shared_Counter is
procedure Increment;
function Value return Natural;
private
Count : Natural := 0;
end Shared_Counter;
protected body Shared_Counter is
procedure Increment is
begin
Count := Count + 1;
end Increment;
function Value return Natural is
begin
return Count;
end Value;
end Shared_Counter;
Auf die Daten eines geschützten Objekts lässt sich ausschließlich über die definierten Operationen zugreifen.
Und der wechselseitige Ausschluss wird von der Sprache garantiert.
procedure Lesen und Schreiben erlaubt, wird exklusiv ausgeführt
function nur lesend, erlaubt die gleichzeitige Ausführung durch mehrere Tasks
entry kann die aufrufende Seite warten lassen, bis eine Bedingung (Barriere) erfüllt ist
In vielen Sprachen ist der wechselseitige Ausschluss tendenziell auf Disziplin angewiesen.
Beim Zugriff auf diese Daten muss dieser Mutex genommen werden
Die Freigabe des Locks darf nicht vergessen werden
Die Reihenfolge der Locks muss eingehalten werden
Bei Adas geschützten Objekten lässt sich „Code, der das Sperren vergessen hat“, von vornherein nicht schreiben.
Denn die Daten und der sie schützende wechselseitige Ausschluss werden als ein einziger Typ deklariert.
Mit entry-Barrierebedingungen lässt sich auch Zustandssynchronisation wie „warten, bis Daten in der Warteschlange ankommen“ schreiben, ohne Flags oder Bedingungsvariablen manuell zu verwalten.
16. SPARK — der Weg zur formalen Verifikation
In der Ada-Welt gibt es einen mächtigen Verbündeten: SPARK.
SPARK ist eine Teilmenge von Ada (ein Subset der Sprache), die so gestaltet ist, dass sich Eigenschaften eines Programms mathematisch beweisen lassen.
procedure Increment (X : in out Integer)
with SPARK_Mode,
Pre => X < Integer'Last,
Post => X = X'Old + 1;
Das SPARK-Werkzeug (GNATprove) beweist zu diesem Code, ohne ihn auszuführen, unter anderem Folgendes.
Dass kein Überlauf auftritt
Dass kein Verstoß gegen Bereichsbeschränkungen auftritt
Dass keine Division durch Null auftritt
Dass keine uninitialisierte Variable gelesen wird
Die Konsistenz von Pre und Post
Der Unterschied zum Testen ist grundlegend.
Test bestätigt korrektes Verhalten für die gewählten Eingaben
Beweis zeigt, dass die Eigenschaft für alle Eingaben gilt
Die in Kapitel 13 gesehenen Verträge (Pre/Post) werden in SPARK unmittelbar zum Gegenstand des Beweises.
Ein als Laufzeitprüfung geschriebener Vertrag lässt sich so nachträglich zu „bewiesen“ hochstufen.
SPARK hat sich in der Luft- und Raumfahrt sowie im Verteidigungsbereich bewährt, doch in den letzten Jahren nimmt die Nutzung auch in der Industrie zu — etwa setzt NVIDIA es für die Firmware-Sicherheit ein.
Die verbreitete Annahme, „formale Methoden seien zu akademisch für die Praxis“, wird von Adas/SPARKs Ökosystem still, aber beharrlich widerlegt.
17. Interoperabilität mit C und C++
Ada ist keine isolierte Sprache.
Die Interoperabilität mit C ist im Anhang B der Sprachspezifikation standardisiert (Annex B — der Anhang des Ada Reference Manual (ARM) mit dem Titel „Interface to Other Languages“, der die Schnittstellen zu anderen Sprachen wie C oder Fortran regelt).
Um beispielsweise die Windows-API-Funktion Sleep aus Ada aufzurufen, schreibt man Folgendes.
with Interfaces.C;
procedure Sleep_Demo is
procedure Sleep (Milliseconds : Interfaces.C.unsigned)
with Import,
Convention => Stdcall,
External_Name => "Sleep";
begin
Sleep (1000);
end Sleep_Demo;
Die Punkte sind:
Import bindet eine externe Implementierung ein
Convention legt die Aufrufkonvention fest (C, Stdcall usw.)
External_Name legt den Symbolnamen beim Linken fest
Interfaces.C stellt Typen bereit, die C-Typen entsprechen (int, unsigned, char* usw.)
Auch die umgekehrte Richtung ist möglich.
Mit Export lässt sich eine in Ada geschriebene Prozedur als von C aufrufbare Funktion veröffentlichen.
Das ermöglicht eine schrittweise Vorgehensweise wie diese.
Eine bestehende C-Bibliothek aus Ada heraus nutzen
Nur den Kern des Systems in Ada/SPARK schreiben, die Peripherie in C/C++ belassen
Ada-Code als DLL bauen und aus anderen Sprachen aufrufen
Ada ist keine Sprache, bei der nur eine komplette Neuimplementierung zum Ziel führt — sie kann mit bestehenden Beständen koexistieren, während sich die Verlässlichkeit schrittweise, beginnend bei den wichtigsten Teilen, erhöhen lässt.
18. Entwicklungsumgebung — GNAT und Alire (funktioniert auch unter Windows)
Man könnte meinen, „um Ada auszuprobieren, braucht man teure Werkzeuge“.
Heute steht dafür kostenlos eine vollwertige Entwicklungsumgebung zur Verfügung.
GNAT der in GCC enthaltene Ada-Compiler (kostenlos)
Alire Adas Paketmanager und Build-Werkzeug
GNAT Studio die IDE von AdaCore
VS Code mit der Ada-Language-Server-Erweiterung stehen Vervollständigung und Sprung zur Definition zur Verfügung
Insbesondere mit dem Erscheinen von Alire (Kommandoname alr) wurde der Einstieg in Ada dramatisch einfacher.
Das Erlebnis ist nahe an Rusts cargo.
alr init --bin hello_ada
cd hello_ada
alr build
alr run
Mit alr init wird das Projekt angelegt, mit alr build gebaut und mit alr run ausgeführt.
Auch die Toolchain (GNAT selbst) holt Alire, sodass nicht einmal eine manuelle Installation des Compilers nötig ist.
Es funktioniert unter Windows, Linux und macOS gleichermaßen.
Wer unter Windows entwickelt, kommt auf folgendem Weg am schnellsten zum Ziel.
1. Den Windows-Installer von der offiziellen Alire-Website herunterladen
2. Mit alr init --bin ein Grundgerüst anlegen
3. Die Ada-Erweiterung (von AdaCore) in VS Code installieren
4. Mit alr build bauen und ausführen
Auch Bibliotheken lassen sich mit alr with <Bibliotheksname> hinzufügen.
Die Zeit, in der man „am Einrichten der Umgebung scheitert“, ist vorbei.
19. Schwächen und Vorbehalte von Ada
Bisher wurde der Reiz von Ada vorgestellt, doch auch Ada hat Schwächen.
Diese sollen hier fair dargestellt werden.
Kleines Ökosystem
Wenige Optionen für Webframeworks, GUIs, Cloud-SDKs usw.
Die Anzahl der Alire-Pakete liegt größenordnungsmäßig unter der von Mainstream-Sprachen
Wenige Fachkräfte und Informationen
Besonders japanischsprachige Informationen sind knapp
Für den Einsatz in Teamentwicklung müssen Schulungskosten eingeplant werden
Die Syntax wirkt umständlich
Typdeklarationen sowie die Trennung von Spezifikation und Rumpf sind für kleine Skripte schwerfällig
Nicht geeignet für „einfach mal schnell etwas zum Laufen bringen“
Begrenzter Stellenmarkt
Stark auf Bereiche wie Luft- und Raumfahrt, Verteidigung und Eisenbahn konzentriert
Auch dass „Ada zu verwenden“ nicht automatisch „sicher“ bedeutet, lehrt uns die Geschichte.
Die Explosion der ersten Ariane-5-Rakete im Jahr 1996 hatte unter anderem in Ada geschriebene Software als Ursache.
Für Ariane 4 geschriebener Code wurde für die Ariane 5 mit ihren anderen Flugeigenschaften wiederverwendet; ein unerwartet großer Wert löste bei der Umwandlung einen Constraint_Error aus, der nicht angemessen behandelt wurde, sodass das System stehen blieb.
Konkret verlief es so: Im Trägheitsreferenzsystem (SRI) gab es eine Verarbeitung, die den vor dem Abheben zur Ausrichtung berechneten Wert BH (Horizontal Bias, einen internen Wert im Zusammenhang mit der horizontalen Geschwindigkeit) von einer 64-Bit-Gleitkommazahl in eine vorzeichenbehaftete 16-Bit-Ganzzahl umwandelte. Die Flugbahn der Ariane 5 erzeugt etwa die fünffache horizontale Geschwindigkeit der Ariane 4, wodurch BH den mit 16 Bit darstellbaren Bereich überschritt und die Umwandlung fehlschlug (im Untersuchungsbericht als „Operandenfehler“ bezeichnet, aus Sicht von Adas Bereichsprüfung eine Umwandlung außerhalb des zulässigen Bereichs). Diese Umwandlung war zudem nicht abgesichert. Weil für den SRI-Rechner das Ziel „maximale Auslastung 80 %“ galt, waren von den sieben riskanten Variablen nur vier abgesichert; bei den übrigen drei war man zu dem Schluss gekommen, dass sie „physikalisch begrenzt sind oder über ausreichend Spielraum verfügen“, und hatte auf eine Absicherung verzichtet. Bei BH traf diese Einschätzung auf die Ariane 5 nicht mehr zu.
Dieser Unfall zeigt Folgendes.
Die Laufzeitprüfung der Sprache hat das Problem erkannt (es ist nicht lautlos zusammengebrochen)
Aber die Betriebsannahmen hatten sich geändert, ohne erneut überprüft zu werden
Das Design für den Fall nach dem Auftreten der Ausnahme (Fail-Safe) war unzureichend
Weder das Typsystem noch Verträge können den Prozess ersetzen, mit dem Annahmen überprüft werden.
Die Sprache ist Teil der Sicherheitstechnik, nicht das Ganze.
Das halte ich für den ehrlichsten Hinweis beim Erlernen von Ada.
20. Langlebige Software und Ada — aus Sicht der Wartung
Auf dieser Website befassen wir uns häufig mit der Wartung und Verlängerung der Lebensdauer bestehender Windows-Bestände.
Aus dieser Perspektive betrachtet, hat Ada einen weiteren Reiz.
Es ist keine Seltenheit, dass in Ada geschriebene Systeme über Jahrzehnte hinweg weiterlaufen.
Und das Sprachdesign von Ada selbst setzt langfristige Wartung voraus.
Trennung von Spezifikation (.ads) und Implementierung (.adb)
-> Ein Wartender kann 20 Jahre später die Schnittstelle allein anhand der Spezifikation erfassen
Starke Typen und Bereichsbeschränkungen
-> Implizite Annahmen bleiben im Code erhalten, statt auf mündliche Überlieferung oder Kommentare angewiesen zu sein
Verträge (Pre/Post)
-> „Das Versprechen dieser Funktion“ bleibt in überprüfbarer Form erhalten
Vollständigkeitsprüfung bei case
-> Der Compiler listet die von einer Spezifikationsänderung betroffenen Stellen auf
Rückwärtskompatibilität wird auch über Standardrevisionen hinweg großgeschrieben
-> Ein Großteil des Ada-83-Codes lässt sich auch mit modernen Compilern noch übersetzen
All das lässt sich unmittelbar als Designrichtlinie auch für die langfristige Wartung in C# oder C++ übernehmen.
Statt int einen aussagekräftigen Typ definieren (einen Typ für eine ID, einen Typ mit einer Einheit)
Typen entwerfen, die keine ungültigen Werte annehmen können (Validierung im Konstruktor)
Öffentliche Schnittstelle und Implementierung bewusst trennen
Vor- und Nachbedingungen über Assertions und Tests ausdrücken
Switch-Anweisungen über Enums vollständig schreiben und Warnungen als Fehler behandeln
Auch wer Ada beruflich nie einsetzt, profitiert davon, Adas Designphilosophie zu lernen.
Als Lehrmaterial für das Gefühl, „Design in Typen auszudrücken“, ist Ada auch heute noch erstklassig.
21. Zusammenfassung
Der Reiz von Ada wurde hier zusammengefasst.
Blicken wir noch einmal auf die zentralen Punkte.
Ada ist eine aktive Sprache, die seit über 40 Jahren in hochverlässlichen Systemen eingesetzt wird
Der Name geht auf Ada Lovelace zurück, der aktuelle Standard ist Ada 2022
Strukturell gleiche, aber unterschiedlich benannte Typen sind verschiedene Typen; eine Einheitenverwechslung wird zum Compile-Fehler
Bereichsbeschränkungen verhindern ungültige Werte bereits auf Typebene
Arrays werden auf ihre Grenzen geprüft, Pufferüberläufe werden nicht zu undefiniertem Verhalten
Pakete trennen Spezifikation und Implementierung, Parametermodi machen den Datenfluss explizit
Generics geben die geforderten Operationen in der Spezifikation an, wodurch Fehler bei der Nutzung eindeutig werden
Die Verträge (Pre/Post) von Ada 2012 lassen die Spezifikation in überprüfbarer Form im Code bestehen
Tasks und geschützte Objekte machen Nebenläufigkeit als Sprachfeature sicher nutzbar
Mit SPARK lassen sich Verträge von der Laufzeitprüfung zum mathematischen Beweis hochstufen
Mit GNAT und Alire lässt es sich kostenlos und sofort ausprobieren, auch unter Windows
Das kleine Ökosystem und der Mangel an Fachkräften sind Schwächen
Die Sicherheitsmechanismen der Sprache ersetzen nicht den Prozess, mit dem Annahmen überprüft werden
Im Sinne von Popularität ist Ada eine Sprache, die nie zum Mainstream wurde.
Doch vieles von dem, was moderne Sprachen als „neues Feature“ einführen — Null-Sicherheit, Vollständigkeitsprüfung, Verträge, eine an Ownership heranreichende Strenge —, besaß Ada bereits seit Jahrzehnten.
Das Wesen von Ada lässt sich in einem Satz zusammenfassen.
Fehler sind nichts, was man findet, sondern etwas, das Typen und Verträge von vornherein unschreibbar machen.
Legen Sie an einem Wochenende mit Alire ein Projekt an und schreiben Sie ein kleines Programm, während der Compiler Sie schimpft.
In dem Moment, in dem Sie merken, dass jeder dieser Compile-Fehler „ein Bug ist, der abgefangen wurde, bevor er zu einem Produktionsausfall wurde“, wird Ihnen der Reiz von Ada einleuchten.
Quellen
- Referenzsammlung der Codeausschnitte dieses Artikels, nach Kapiteln geordnet - komurasoft-blog-samples (GitHub)
- Ada Programming Language - AdaCore
- Learn Ada - AdaCore (learn.adacore.com)
- Introduction to Ada - learn.adacore.com
- Ada Reference Manual (Ada 2022)
- Alire - Ada Library Repository
- GNAT User’s Guide - GCC
- SPARK - AdaCore
- Introduction to SPARK - learn.adacore.com
- Ada Conformity Assessment Authority
- Ariane 501 Inquiry Board Report (ESA)
Verwandte Artikel
Aktuelle Artikel mit denselben Schlagwörtern führen zu verwandten Themen weiter.
Generische Programmierung in Ada ── Verträge in Typen schreiben und Wiederverwendung ohne Laufzeitkosten
Eine systematische Einführung in die generische Programmierung in Ada - von generischen Unterprogrammen und Paketen über formale Unterpro...
Einführung in die formale Verifikation mit SPARK ── Von Ada-Verträgen zum mathematischen Beweis
Eine praxisorientierte Einführung in die formale Verifikation mit SPARK, der Ada-Teilsprache. Der Artikel zeigt den Weg von Verträgen (Pr...
Echtzeitsystemprogrammierung mit Ada — Priorität, Periodizität und Ausführungszeitsteuerung in der Praxis
Ein praxisnaher Einstieg in Adas Annex D (Echtzeitsysteme) anhand von acht praktischen Codebeispielen: Task-Prioritäten, Ceiling_Locking,...
Sichere Nebenläufigkeit mit Ada — Ein praktischer Leitfaden zu Tasks und geschützten Objekten
Ein Einführungsartikel zu Adas sprachintegrierter Nebenläufigkeit mit Tasks und geschützten Objekten. Er behandelt Rendezvous (entry/acce...
Prüfung zum Registered Information Security Specialist – Frühjahr 2024 (Reiwa 6), Nachmittag, Aufgabe 1 erklärt – JWT alg=none, API-Autorisierung und vorläufige WAF-Abwehr
Anhand von Aufgabe 1 der Nachmittagsprüfung Frühjahr 2024 (Reiwa 6) zum Registered Information Security Specialist erklärt dieser Artikel...
Verwandte Themen
Diese Seiten ordnen den Artikel in einen größeren Leistungs- und Entscheidungskontext ein.
Technische Windows-Themen
Portal zu Windows-Entwicklung, Fehleranalyse und der Nutzung bestehender Assets.
Häufige Fragen
Fragen, die in Beratungen zu diesem Artikelthema häufig gestellt werden.
- Wird die Sprache Ada heute noch verwendet?
- Ja, sie wird verwendet. In hochverlässlichen Systemen, bei denen ein Fehler unmittelbar Menschenleben oder enorme Verluste kostet — Flugsteuerungen ziviler Flugzeuge, Flugsicherung, Signal- und Sicherungssysteme der Eisenbahn, Raketen und Satelliten, Verteidigungssysteme, Medizingeräte —, wird Ada seit Jahrzehnten kontinuierlich eingesetzt. Ada ist eine seit über 40 Jahren fortlaufend weiterentwickelte Sprache: Sie begann 1983 mit Ada 83, durchlief Ada 95, Ada 2005 und Ada 2012, und der aktuelle Standard ist Ada 2022.
- Was unterscheidet die starke Typisierung von Ada von anderen Sprachen?
- In Ada werden Typen, die unter verschiedenen Namen deklariert wurden, auch dann als unterschiedliche Typen behandelt, wenn ihre Struktur völlig identisch ist. Werden beispielsweise die Typen Meters und Seconds beide aus Float abgeleitet, führt eine Vermischung zu einem Compile-Fehler, und eine Umwandlung muss explizit geschrieben werden. Darüber hinaus kann einem Typ über ein Subtype ein Wertebereich (etwa 0 bis 100) mitgegeben werden; ein Verstoß löst zur Laufzeit die Ausnahme Constraint_Error aus. Fehler wie eine Einheitenverwechslung werden so nicht durch „Vorsicht“, sondern dadurch verhindert, dass der Build von vornherein nicht durchläuft.
- Wie kann ich die Sprache Ada kostenlos ausprobieren?
- Mit GNAT (dem in GCC enthaltenen, kostenlosen Ada-Compiler) und Alire (Adas Paketmanager und Build-Werkzeug, Kommandoname alr) lässt sich unter Windows, Linux und macOS gleichermaßen kostenlos eine Entwicklungsumgebung einrichten. Man lädt den Installer von der offiziellen Alire-Website herunter, legt mit alr init --bin ein Grundgerüst an, baut mit alr build und führt mit alr run aus — ein Erlebnis nahe an Rusts cargo. Da Alire auch die eigentliche Toolchain selbst besorgt, ist keine manuelle Installation des Compilers nötig. Für VS Code gibt es eine Ada-Erweiterung von AdaCore.
- Was sind die Schwächen der Sprache Ada?
- Zu nennen sind ein kleines Ökosystem mit deutlich weniger Auswahl bei Webframeworks, GUIs und Cloud-SDKs als in Mainstream-Sprachen, ein Mangel an Fachkräften und Informationen (insbesondere auf Japanisch), sodass Schulungskosten einzuplanen sind, eine Syntax mit Typdeklarationen und der Trennung von Spezifikation und Implementierung, die sich für kleine Skripte schwerfällig anfühlt, sowie ein Stellenmarkt, der stark auf Luft- und Raumfahrt, Verteidigung und Eisenbahn konzentriert ist. Wie der Ariane-5-Unfall von 1996 zeigt, ist außerdem zu beachten, dass die Sicherheitsmechanismen der Sprache keinen Ersatz für den Prozess bieten, mit dem Annahmen überprüft werden.
Autorenprofil
Profilseite des Artikelautors.
Go Komura
Geschäftsführer von KomuraSoft LLC
Spezialisiert auf Windows-Softwareentwicklung, technische Beratung und Fehleranalyse, insbesondere bei bestehenden Systemen und schwer reproduzierbaren Störungen.