Spezifikationssprache

Bevor jemand ein Programm schreibt, muss klar sein, was das Programm können soll. Solche Anforderungen werden oft in normalem Deutsch notiert, etwa: « Ein Geldautomat darf nie mehr Geld ausgeben, als auf dem Konto liegt. » Genau da liegt das Problem, denn Alltagssprache ist mehrdeutig und lässt Lücken offen. Eine Spezifikationssprache ist eine künstliche Sprache mit streng festgelegten Regeln, in der man dieselbe Forderung eindeutig aufschreibt. Sie beschreibt das gewünschte Verhalten, nicht den Weg dorthin. Der Unterschied zu einer Programmiersprache ist wichtig: Programmiersprachen sagen einem Rechner Schritt für Schritt, was er tun soll. Eine Spezifikationssprache sagt nur, welches Ergebnis am Ende gelten muss.

Warum Eindeutigkeit bei Software über Leben entscheiden kann

Die meisten schweren Softwarefehler entstehen nicht beim Tippen des Codes. Sie entstehen viel früher, weil zwei Beteiligte unter derselben Anforderung etwas Verschiedenes verstanden haben. Ein Satz wie « Das System soll schnell reagieren » ist für den einen eine Sekunde, für den anderen eine Minute. Eine Spezifikationssprache zwingt dazu, solche Angaben zu präzisieren, bevor Geld in die Entwicklung fließt.

Besonders wichtig wird das dort, wo ein Fehler teuer oder gefährlich ist. Bremssysteme in Autos, Steuerungen in Flugzeugen, Chips in Rechenzentren und Banksoftware werden deshalb häufig formal spezifiziert. Ein berühmtes Beispiel ist ein Rechenfehler in einem Intel-Prozessor aus dem Jahr 1994. Der Rückruf kostete das Unternehmen damals etwa 475 Millionen US-Dollar. Seither prüfen Chiphersteller ihre Entwürfe systematisch gegen formale Beschreibungen.

Ein zweiter Vorteil ist die Prüfbarkeit. Weil eine Spezifikation mathematisch eindeutig ist, kann eine Software sie automatisch mit dem tatsächlichen Programm vergleichen. Man nennt das formale Verifikation. Testen zeigt immer nur, dass in den geprüften Fällen nichts schiefging. Eine Verifikation kann dagegen zeigen, dass ein Fehler in keinem Fall auftritt.

Zusicherungen, Zustände und der Blick des Prüfers

Die meisten Spezifikationssprachen bauen auf Logik und Mengenlehre auf, also auf Mathematik aus der Schule. Häufig beschreibt man drei Dinge: die Vorbedingung, die Nachbedingung und die Invariante. Die Vorbedingung sagt, was gelten muss, damit eine Funktion überhaupt aufgerufen werden darf. Die Nachbedingung sagt, was danach gelten muss. Eine Invariante ist eine Aussage, die zu jedem Zeitpunkt wahr bleiben muss.

Beim Geldautomaten wäre die Invariante: Der Kontostand ist nie negativ. Die Vorbedingung einer Auszahlung wäre: Der gewünschte Betrag ist kleiner oder gleich dem Guthaben. Die Nachbedingung wäre: Der neue Kontostand ist der alte minus dem ausgezahlten Betrag. Ein Prüfprogramm rechnet nun alle möglichen Fälle durch. Findet es einen Ablauf, der die Invariante verletzt, meldet es ein Gegenbeispiel.

Man kann sich das wie einen Bauplan mit Statik-Nachweis vorstellen. Der Plan sagt nicht, in welcher Reihenfolge die Handwerker arbeiten. Er legt fest, welche Lasten das Gebäude aushalten muss. Ein verbreiteter Irrtum ist, eine Spezifikation mache Fehler unmöglich. Sie garantiert nur, dass das Programm zur Beschreibung passt. Ist die Beschreibung selbst falsch gedacht, hilft auch die beste Prüfung nicht.

Von TLA+ bis zum Prompt: Wo formale Beschreibungen auftauchen

Bekannte Vertreter sind TLA+, Z, Alloy und die Sprache VDM. Amazon setzt TLA+ seit Jahren ein, um die Abläufe seiner Cloud-Dienste zu prüfen. Ingenieure fanden damit Fehler, die in normalen Tests jahrelang unentdeckt geblieben wären. In der Chipentwicklung ist die Sprache SystemVerilog Assertions Standard. Wer Meldungen über Halbleiter oder Cloud-Infrastruktur liest, begegnet diesen Begriffen regelmäßig.

Auch abgeschwächte Formen sind im Alltag verbreitet. Wenn eine Programmierschnittstelle im Internet genau festlegt, welche Daten sie erwartet und zurückgibt, ist das eine Spezifikation in Textform. Formate wie OpenAPI oder JSON Schema erfüllen diese Aufgabe, ohne vollständige Mathematik zu verlangen.

Neuen Auftrieb bekommt das Thema durch KI-Programmierhilfen. Modelle schreiben inzwischen große Mengen Code, den niemand mehr Zeile für Zeile liest. Damit wird die Frage wichtiger, woran man überhaupt misst, ob dieser Code korrekt ist. Manche Forscher sehen die Spezifikation deshalb als eigentliche Arbeit des Menschen. Der Mensch beschreibt präzise das Ziel, die Maschine erzeugt und prüft den Weg.