Softwareentwicklung ist heute ein integraler Bestandteil nahezu aller Branchen. Ob im Banking, in der Medizin oder bei der Lieferung von Paketen – Programme steuern und automatisieren Prozesse in unserer Welt. Doch trotz all der fortschrittlichen Werkzeuge und hohen Investitionen bleibt die Erstellung fehlerfreier Software eine große Herausforderung. Der Grund dafür ist nicht nur ungenügende Technik oder mangelndes Wissen, sondern tief in den wissenscha¿flichen Grundsätzen der Computerwissenschaften verwurzelt. Das Schreiben von korrekter Software ist sowohl praktisch als auch theoretisch schwierig, und genau dieser Diskurs erklärt, warum.
Der Ursprung dieses Dilemmas liegt in der theoretischen Informatik, die sich vor gut einem Jahrhundert aus der mathematischen Logik entwickelte. Die Intention war damals, Mathematik komplett formal zu erfassen, um Konsistenz, Vollständigkeit und Entschei- dungsfähigkeit zu beweisen. David Hilbert stellte das ambitionierte Ziel auf, dass jeder wahre mathematische Satz bewiesen werden kann, und es einen Algorithmus gäbe, der entscheiden kann, ob ein Beweis existiert – das Entscheidungsproblem. Doch Kurt Gödel und später Alonzo Church sowie Alan Turing widerlegten diese Hoffnungen fundamental. Gödel zeigte, dass es immer wahre Aussagen gibt, die nicht innerhalb eines formalen Systems bewiesen werden können.
Church und Turing bewiesen, dass es keinen Algorithmus geben kann, der für jedes Programm entscheidet, ob es jemals hält oder in einer Endlosschleife feststeckt – der Satz vom Halteproblem. Die Konsequenzen dieser Grundsätze sind weitreichend: Programme können grundsätzlich nicht vollständig verstanden oder verifiziert werden, da es keine allumfassende Methode gibt, ihr Verhalten für alle Inputs vorauszusagen. Wesentlich ist hier Rice’s Theorem, das besagt, dass für jede nicht-triviale Eigenschaft von Programmen kein Algorithmus existiert, der entscheiden kann, ob dieses Programm diese Eigenschaft besitzt. Etwa ob ein Programm immer korrekte Quadratzahlen ausgibt, kann nicht generell automatisiert ermittelt werden. Entscheidungsprobleme wie das Erreichen bestimmter Programmzustände sind somit unentscheidbar.
Noch komplexer zeigt sich die sogenannte Busy-Beaver-Funktion, die ausdrückt, wie lange ein Programm mit n Steuerzuständen maximal läuft, bevor es hält. Diese Funktion ist nicht berechenbar, und daraus folgt, dass wir selbst die Aufwände für das Überprüfen von Programmen nicht abschätzen können. Proofs über die Terminierung eines Programms können ebenfalls extrem groß oder sogar nicht existieren, was die Verifikation weiter erschwert. Selbst wenn man die langwierigen, theoretischen Limitationen außen vorlässt, macht die Komplexität vieler Programmieraufgaben das Schreiben fehlerfreier Software schwer. Bei der Verifikation stellt sich daher die Frage nach praktischen Grenzen: Wie stark kann man Programme einschränken, damit eine Korrektheitsüberprüfung machbar wird und wie effektiv sind existierende Methoden? Eine erwartete Vereinfachung wäre, Programme in mäßiger Komplexität oder in sogenannten totalen Sprachen zu schreiben, in denen jede Funktion zwangsläufig terminiert.
Solche Sprachen erzwingen oft Schleifenzähler oder Rekursion mit abnehmenden Argumenten. Interessanterweise hilft das nicht wirklich. Zum Beispiel sind selbst Programme mit sehr einfachen Schleifen und Operationen, die nur Terminierung erlauben, oft unentscheidbar in ihrer Verifikation. Ein herausragendes Symbol ist ein Programm, das den Algorithmus dahinter Goldbachs Vermutung kodiert – eines der seit Jahrhunderten ungelösten Probleme der Zahlentheorie. Obwohl das Programm leicht lesbar ist, konnte bis heute niemand beweisen, dass es niemals in einen Fehlerzustand gelangt.
Die Suche nach praktikablen Grenzen führte die Forschung zu endlichen Automaten, den einfachsten Modellen mit endlich vielen Zuständen. Für diese Modelle gibt es durchaus automatisierte Model-Checker, die Properties und Korrektheit relativ effizient überprüfen können. Dennoch trifft man auch hier auf das Problem der Zustands-Explosion: Die Zustandsräume wachsen exponentiell mit der Anzahl von Variablen oder parallel laufenden Komponenten, was die Leistungsfähigkeit von Verifikationstools stark limitiert. Eine grundlegende Erkenntnis ist: Korrektheit lässt sich nicht einfach auf Module oder Programmteile reduzieren. Selbst wenn kleine Teile gut verifizierbar sind, kann die Zusammensetzung der Teile ein völlig unübersichtliches und schwer überprüfbares System ergeben.
Das stellt eine fundamentale Hürde für modulare Softwareentwicklung und einfache Verifikationstechniken dar. Ein weiterer Irrglaube ist, dass höhere Sprachebenen und Abstraktionen die Verifikation erleichtern. Tatsächlich erhöhen Konzepte wie Variablenzustände, Nebenläufigkeit oder Rekursion die inhärente Komplexität exponentiell und erschweren die Analyse. Einzige Ausnahme ist die sogenannte Hierarchie als Abstraktion, die in bestimmten Fällen die Verifikationskomplexität nur polynomiell steigen lässt. Moderne Tools zur Softwareverifikation teilen sich in verschiedene Kategorien: Model-Checker, sektorspezifische statische Analysetools, deduktive Verifikation mit formalen Beweisen und Typensysteme, die eine Form der leichten Verifikation bieten.
Während Model-Checker für endliche Modelle gut funktionieren, sind deduktive Beweise oft sehr aufwendig und erfordern Expertenwissen. Statische Analyse liefert oft nur unvollständige Resultate und kann „unsicher“ sein – also Fälle melden, die keine echten Fehler sind, oder Fehler übersehen. Typ-Systeme helfen dabei, bestimmte Fehlerklassen zu verhindern und verbessern die Sicherheit, sind aber prinzipiell eingeschränkt, da sie nur weniger komplexe Eigenschaften prüfen. In der Praxis ist das Zusammenspiel dieser Methoden entscheidend, um akzeptable Softwarequalität zu erreichen. Die extremen Limitationen erfordern eine Kombination aus automatischer Analyse, menschlicher Intuition, Erfahrung und empirischem Know-How.
Die Vielzahl der Beweise und theoretischen Resultate zeigt, dass die Schwierigkeit bei der Erstellung korrekter Software eine fundamentale, unüberwindbare Grenze darstellt. Diese Probleme sind nicht auf schlechte Implementierungen zurückzuführen, sondern deren Ursache ist in den grundlegenden Gesetzen der Berechenbarkeit und Komplexität verwurzelt. Angesichts dieser Tatsache plädiert die Forschung für mehr empirische Untersuchungen: Nicht alle Programme sind gleich komplex, und die vielfältigen Programme, die Menschen täglich schreiben, zeigen Muster, die durch systematische Studien erfasst werden können. Ein besseres Verständnis der realen Softwarelandschaft, ihrer Fehlerursachen und der Eigenschaften von Fehlern kann dabei helfen, praktikable Methoden und Werkzeuge zu entwickeln, die in der Praxis wirksam sind. Daran anknüpfend macht eine aktuelle Untersuchung von Ausfällen großer verteilter Systeme deutlich, dass viele Fehler durch mangelnde Beachtung von Fehlerbehandlungs-Code entstehen.
