Assertion (Informatik)

Was ist eine Zusicherung?

Eine Zusicherung (auch Sicherstellung oder Assertion) ist eine Aussage über den Zustand eines Computerprogramms oder einer elektronischen Schaltung. Mit Zusicherungen lassen sich logische Fehler im Programm oder Defekte in der umgebenden Hard- und Software erkennen, woraufhin das Programm kontrolliert beendet werden kann. Bei der Entwicklung elektronischer Schaltungen dienen Assertions dazu, in der Verifikationsphase die Einhaltung der Spezifikation zu prüfen und Informationen über den Grad der Testabdeckung zu liefern.

Anwendung und Abgrenzung zur Fehlerbehandlung

Mit einer Zusicherung bringt der Entwickler zum Ausdruck, dass er bestimmte Bedingungen während der Laufzeit für stets wahr hält – sie werden Teil des Programms. Diese Überzeugungen werden von den normalen Laufzeitumständen getrennt; Abweichungen werden nicht regulär behandelt, damit nicht die Vielzahl möglicher Fehlerfälle die eigentliche Problemlösung erschwert (z. B. wenn Variablen durch Fehler im Betriebssystem überschrieben wurden und 2+2=4 plötzlich nicht mehr gilt). Zusicherungen unterscheiden sich dadurch von klassischer Fehlerbehandlung mit Kontrollstrukturen oder Ausnahmen (Exceptions), die einen Fehlerfall als mögliches Ergebnis einschließen. Faustregel: Fehlerbehandlungen schreibt man für Fehlerzustände, mit denen man rechnet; Zusicherungen für Fehlerzustände, die niemals auftreten sollten. In manchen Programmiersprachen sind Zusicherungen auf Sprachebene eingebaut, häufig als Sonderform der Ausnahmen verwirklicht.

Geschichte

Der Begriff assertion wurde 1967 von Robert Floyd im Artikel Assigning Meanings to Programs eingeführt. Er schlug eine Methode vor, die Korrektheit von Flussdiagrammen zu beweisen, indem man jedes Element mit einer Zusicherung versieht; dafür gab er Regeln an. Tony Hoare entwickelte dies zum Hoare-Kalkül für prozedurale Programmiersprachen weiter: Eine Zusicherung vor einer Anweisung heißt Vorbedingung (precondition), eine nach der Anweisung Nachbedingung (postcondition), eine Zusicherung, die bei jedem Schleifendurchlauf erfüllt sein muss, heißt Invariante. Niklaus Wirth nutzte Zusicherungen zur Definition der Semantik von Pascal und empfahl Programmierern, Zusicherungen als Kommentare zu schreiben – daher werden Kommentare in Pascal mit geschweiften Klammern {…} umgeben, wie Hoare es in seinem Kalkül verwendete.

Zusicherungen in Programmiersprachen und Hardwareverifikation

In Borland Delphi ist die Idee als System-Funktion assert eingebaut; in Java gibt es ab Version 1.4 das Schlüsselwort assert. In Java wird das Programm bei einer verletzten Zusicherung nicht notwendigerweise beendet, sondern es wird eine Ausnahme (exception) ausgelöst, die das Programm weiterverarbeiten kann. Beispiel in Java: Nach int n = readInput(); n = n * n; folgt assert n >= 0; – der Programmierer sagt damit: „Ich bin mir sicher, dass nach dieser Stelle n größer gleich null ist.“ Bertrand Meyer hat Zusicherungen im Paradigma Design by contract verarbeitet und in der Programmiersprache Eiffel umgesetzt: Vorbedingungen werden durch require-Klauseln, Nachbedingungen durch ensure-Klauseln beschrieben, für Klassen können Invarianten spezifiziert werden; bei Verletzung wird eine Ausnahme ausgelöst. In C kann man über die Header-Datei assert.h das Makro assert verwenden. Bei Fehlschlag gibt es eine Standardmeldung mit der Bedingung, dem Dateinamen und der Zeilennummer aus, z. B.: Assertion „s!=NULL“ failed in file „C:/Projects/Sudoku/utils.c“, line 9. Beispiel: eine Funktion strlenChecked prüft mit assert(s != NULL), ob der übergebene Zeiger nicht NULL ist, bevor strlen aufgerufen wird (strlen prüft das nicht selbst). Hardwarebeschreibungssprachen wie VHDL und SystemVerilog unterstützen ebenfalls Assertions; PSL ist eine eigenständige Beschreibungssprache für Assertions, die Modelle in VHDL, Verilog und SystemC unterstützt. Bei der Verifikation erfasst das Simulationswerkzeug, wie oft die Assertion ausgelöst wurde und wie oft die Zusicherung erfüllt oder verletzt wurde. Wurde sie ausgelöst und nie verletzt, gilt die Schaltung als erfolgreich verifiziert; wurde sie nie ausgelöst, fehlt Testabdeckung und die Verifikationsumgebung muss erweitert werden.

Verwandte Techniken: Umformulieren des Quelltextes

Assertions entdecken Programmfehler erst zur Laufzeit beim Anwender, also oft zu spät. Deshalb versucht man, logische Fehler bereits zur Kompilierzeit durch den Compiler als Fehler und Warnungen aufzudecken, indem man den Quelltext geeignet formuliert – z. B. Fallunterscheidungen auf ein Minimum reduziert, sodass manche Fehler gar nicht mehr ausdrückbar und damit unmöglich sind. Das Beispiel einer Java-Enumeration TURN mit den Werten LEFT_TURN und RIGHT_TURN zeigt in einer switch-Anweisung einen default-Fall mit assert false: „Es gibt nur Links- oder Rechtskurven“, der nicht auftreten kann. Alternativ kann man statt der speziellen Kodierung einen einfachen Wahrheitswert (boolean isLeftTurn) verwenden – dabei wird der Code allerdings oft weniger explizit und unverständlicher. Fehler, die auch so nicht gefunden werden, können häufig mittels Modultests aufgedeckt werden.

Zusicherungen zur Kompilierzeit

Während normale Assertions zur Laufzeit geprüft werden, kann man in C++ Bedingungen auch schon beim Übersetzen prüfen. Nur Bedingungen, die zur Übersetzungszeit bekannt sind, sind nachprüfbar, z. B. sizeof(int) == 4. Früher geschah dies compilerabhängig und mit gewöhnungsbedürftigen Formulierungen, etwa über den Präprozessor mit #if sizeof(int) != 4 / #error „unerwartete int-Größe“ oder über einen Trick mit der Array-Größe int valid[sizeof(int)==4]; – schlug der Test fehl, ließ sich das Programm nicht übersetzen (der Compiler meldete, dass Arrays mindestens ein Element haben müssen). Mit C11 bzw. C++11 wurden dafür die Schlüsselworte _Static_assert bzw. static_assert eingeführt (in C11 zusätzlich als Makro implementiert), z. B. static_assert(sizeof(int)==4, „…“).