Assertion (Informatik)

Aussage über den Zustand eines Computer-Programms oder einer elektronischen Schaltung
Dies ist eine alte Version dieser Seite, zuletzt bearbeitet am 12. Dezember 2007 um 16:40 Uhr durch 87.234.62.242 (Diskussion) (Anwendung). Sie kann sich erheblich von der aktuellen Version unterscheiden.

Eine Zusicherung oder Assertion (lat./engl. für Aussage; Behauptung) ist eine Aussage über den Zustand eines Computer-Programmes. Mit Hilfe von Zusicherungen können logische Fehler im Programm oder Defekte in der umgebenden Hard- oder Software erkannt und das Programm kontrolliert beendet werden.

Anwendung

Durch die Formulierung einer Zusicherung bringt der Entwickler eines Programms seine Überzeugung über bestimmte Bedingungen während der Laufzeit eines Programms zum Ausdruck und lässt sie Teil des Programms werden. Er trennt diese Überzeugungen von den normalen Laufzeitumständen ab und nimmt diese Bedingungen als stets wahr an. Abweichungen hiervon werden nicht regulär behandelt, damit die Vielzahl möglicher Fälle nicht die Lösung des Problems vereitelt, denn natürlich kann es während der Laufzeit eines Programms dazu kommen, dass 2+2=4 einmal nicht gilt, z.B. weil Variablen durch Programmfehler im Betriebssystem überschrieben wurden.

Damit unterscheiden sich Zusicherungen von der klassischen Fehlerkontrolle durch Kontrollstrukturen oder Ausnahmen (Exceptions), die einen Fehlerfall als mögliches Ergebnis einschließen. In einigen Programmiersprachen wurden Zusicherungen auf Sprachebene eingebaut, häufig werden sie als Sonderform der Ausnahmen verwirklicht.

Geschichte

Eingeführt wurde der Begriff Assertion von Robert Floyd 1967 in seinem Artikel Assigning Meanings to Programs. Er schlug eine Methode vor, mit der man die Korrektheit von Flussdiagrammen beweisen konnte indem man jedes Element des Flussdiagramms mit einer Zusicherung versieht. Floyd gab Regeln an, nach denen die Zusicherungen bestimmt werden konnten. Tony Hoare entwickelte diese Methode zum Hoare-Kalkül für prozedurale Programmiersprachen weiter. Im Hoare-Kalkül wird eine Zusicherung, die vor einer Anweisung steht, Vorbedingung (engl. precondition), eine Zusicherung nach einer Anweisung Nachbedingung (engl. postcondition) genannt. Eine Zusicherung, die bei jedem Schleifendurchlauf erfüllt sein muss, heißt Invariante.

Niklaus Wirth benutzte Zusicherungen zur Definition der Semantik von Pascal und schlug vor, dass Programmierer in ihre Programme Kommentare mit Zusicherungen schreiben sollten. Aus diesem Grund sind Kommentare in Pascal mit geschweiften Klammern {...} umgeben, eine Syntax, die Hoare in seinem Kalkül für Zusicherungen verwendet hatte.

In Delphi wurde die Idee übernommen und ist als System-Funktion assert eingebaut. In der Programmiersprache Java steht seit Version 1.4 das Schlüsselwort assert zur Verfügung.

Programmierpraxis

In der Programmiersprache C könnte eine Zusicherung in etwa so eingesetzt werden:

#include <assert.h>
/// diese Funktion liefert die Länge eines nullterminierten Strings
/// falls der übergebene auf die Adresse NULL verweist, wird das
/// Programm kontrolliert abgebrochen. (strlen prüft das nicht selbst)
int strlenChecked(char* s) {
  assert(s != NULL);
  return strlen(s);
}

In diesem Beispiel wird über die Einbindung der Header-Datei assert.h das Makro assert verwendbar. Dieses Makro sorgt im Falle eines Fehlschlags für die Ausgabe einer Standardmeldung, in der die nicht erfüllte Bedingung zitiert wird und Dateiname und Zeilennummer hinzugefügt werden. Eine solche Meldung sieht dann so aus:

Assertation "s!=NULL" failed in file "C:\Projects\Sudoku\utils.c", line 9

Beim Übersetzen kann man einstellen, dass die Zusicherungen zur Laufzeit nicht überprüft werden, indem man NDEBUG vor der Einbindung von assert.h definiert. Dies wird üblicherweise bei Release-Builds des Programms gemacht. So erhält man eine Programmversion die etwas schneller läuft. Man sollte das wenn irgend möglich vermeiden, denn fehlgeschlagene Zusicherungen haben nichts mit normalen (durch das Programm verkraftbaren) Fehlerfällen zu tun, im Gegenteil eine fehlgeschlagene Zusicherung bedeutet, dass ein Programm am Ende ist, die Laufzeitkosten für eine Prüfung sind ohnehin oft gering. Wer darauf vertrauen will, dass all seine Release-Versionen geprüfte Zusicherungen enthalten, lösche die Definition von NDEBUG vor dem Einbinden von assert.h.

Beim Verwenden von Zusicherungen sollte darauf geachtet werden, dass je nach Definition von NDEBUG das Programm auch seine Funktionsweise verändern kann, nämlich falls in der Berechnung Nebeneffekte auftreten. Man sollte solche Nebeneffekte meiden:

// falls die Zusicherungen abgeschaltet werden, wird die Funktion
// BerechneSteuerSatz nicht mehr aufgerufen
// dadurch ändert sich der Programmablauf
assert(BerechneSteuerSatz(betrag, steuer1, steuer2) == true);
// oder kurz
assert(BerechneSteuerSatz(betrag, steuer1, steuer2));

Java kennt das Konzept der Zusicherungen ab Version 1.4. Hier wird allerdings das Programm nicht notwendigerweise beendet, sondern eine so genannte Ausnahme (englisch exception) geworfen, die innerhalb des Programms weiter verarbeitet werden kann.

Ein einfaches Beispiel einer Assertion (hier in Java-Syntax) ist

int n = readInput();
n = n * n; //Quadrieren
assert n >= 0;

Mit dieser Assertion sagt der Programmierer "Ich bin mir sicher, dass nach dieser Stelle n größer gleich null ist".

Bertrand Meyer hat die Idee von Zusicherungen in dem Programmierparadigma 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. Auch in Eiffel werden Ausnahmen geworfen, wenn eine Zusicherung nicht erfüllt ist.

Verwandte Techniken

Assertations entdecken Programmfehler zur Laufzeit, beim Anwender, also erst wenn es zu spät ist. Um Meldungen über "Interne Fehler" möglichst zu vermeiden, versucht man durch geeignete Formulierung des Quelltextes logische Fehler bereits zur Kompilierzeit (durch den Compiler) in Form von Fehlern und Warnungen aufdecken zu lassen. Logische Fehler, die man auf diese Weise nicht finden kann, können häufig mittels Modultests aufgedeckt werden.

Umformulieren des Quelltextes

Indem Fallunterscheidungen auf ein Minimum reduziert werden, ist mancher Fehler nicht ausdrückbar, dann ist er als logischer Fehler auch nicht möglich. Nehmen wir an es gäbe nur zwei mögliche Fälle (das ist in der Tat häufig so) dann könnten wir einen einfachen Wahrheitswert verwenden anstelle einer spezielleren Kodierung:

/// Funktion liefert den Text zu einem Geschlechtskode
const char* genderStr(bool isFemale) {
  return isFemale ? "weiblich" : "männlich";
}

auch wenn es politisch korrekter wäre, enthält das folgende Beispiel eine (scheinbar) absurde Fehlermöglichkeit:

/// Geschlechtskennung als Enumeration:
enum GENDER { GENDER_MALE, GENDER_FEMALE };
/// Funktion liefert den Text zu einem Geschlechtskode
const char* genderStr(GENDER gender) {
  switch(gender) {
    case GENDER_FEMALE: return "weiblich";
    case GENDER_MALE:   return "männlich";
    default:            assert(0); return ""; // ???
  }
}

Zusicherungen zur Kompilierzeit

Während die oben beschriebenen Assertionen zur Laufzeit des Programms geprüft werden, gibt es in C++ die Möglichkeit, Bedingungen auch schon beim Übersetzen des Programms durch den Compiler zu überprüfen. Es können nur Bedingungen nachgeprüft werden, die zur Übersetzungszeit bekannt sind, z. B. sizeof(int) == 4. Schlägt ein Test fehl, lässt sich das Programm nicht übersetzen:

#if sizeof(int) != 4
  #error "unerwartete int-Größe"
#endif

Allerdings hängt das stark von der Funktionalität des jeweiligen Compilers ab und manche Formulierungen sind gewöhnungsbedürftig:

/// Die Korrektheit unserer Implementierung hängt davon ab, 
/// dass ein int 4 Bytes groß ist. Falls dies nicht gilt, 
/// bricht der Compiler mit der Meldung ab, dass 
/// Arrays mindestens ein Element haben müssen:
void validIntSize(void) {
  int valid[sizeof(int)==4];
}

Zusicherungen in Modultests

Ein Bereich in dem ebenfalls Zusicherungen eine Rolle spielen, sind Modultests (entwickelt für und Kernbestandteil des Extreme Programmings). Wann immer man am Quelltext Änderungen (z.B. Refactorings) vornimmt, z.B. um weitere Funktionen zu integrieren, führt man Tests auf Teilfunktionen (Modulen, also z.B. Funktionen Prozeduren, Klassen) aus, um die bekannte (gewünschte) Funktionalität zu evaluieren.

Im Gegensatz zu assert wird bei einem Fehlschlag nicht das ganze Programm beendet, sondern nur der Test als gescheitert betrachtet und weitere Tests ausgeführt, um möglichst viele Fehler zu finden. Laufen alle Tests fehlerfrei, dann sollte davon ausgegangen werden können, dass die gewünschte Funktionalität besteht.

Von besonderer Bedeutung ist der Umstand, dass Modultests üblicherweise nicht im Produktivcode ausgeführt werden, sondern zur Entwicklungszeit. Das bedeutet, dass Assertions im fertigen Programm als Gegenpart zu betrachten sind, man sollte sich also nicht für das eine oder das andere entscheiden, sondern beides benutzen.

Spezielle Techniken für Microsoft-Compiler

Neben Assert wird häufig auch Verify verwendet. Verify führt alle Anweisungen, die in die Berechnung der Bedingung einfließen aus , gleichgültig, ob mit oder ohne Debug-Absicht kompiliert wurde. Die Überprüfung findet aber nur in der Debug-Variante statt, d.h. auch hier kann ein Programm in obskurer Weise scheitern, falls die Zusicherung nicht erfüllt ist.

// die Variable anzahl wird immer erhöht
Verify(++anzahl>2);

Assert_Valid wird eingesetzt, um Objekte auf ihre Gültigkeit zu testen. Dazu gibt es in der Basisklasse der Objekthierarchie die virtuelle Methode AssertValid(). Die Methode sollte für jede konkrete Klasse überschrieben werden, um die internen Felder der Klasse auf Gültigkeit zu testen.

// Example for CObject::AssertValid.
void CAge::AssertValid() const
{
  CObject::AssertValid();
  ASSERT( m_years > 0 );
  ASSERT( m_years < 105 );
}

Literatur

  • Robert W. Floyd: Assigning meanings to programs, Proceedings of Symposia in Applied Mathematics, Volume 19 (1967), Seite 19-32