Formale Methoden in der Softwarequalität

Formale Methoden sind mathematisch fundierte Techniken, mit denen sich bestimmte Eigenschaften von Software beweisen lassen. Statt weniger Beispiele zeigen sie allgemeingültig, dass ein Programm eine Spezifikation erfüllt. Grundlage ist meist funktionale Programmierung, weil dort Code aus Gleichungen besteht und sich damit direkt mathematisch schlussfolgern lässt.

Das Wichtigste in Kürze

• Formale Methoden liefern keinen Beweis, dass Software “absolut richtig” ist, sondern steigern die Redundanz so massiv, dass ein unentdeckter Fehler praktisch ausgeschlossen wird.
• Funktionale Programmierung reduziert den Abstand zwischen Code und Mathematik, weil jede Funktion eine Gleichung definiert und damit “Gleiches durch Gleiches” ersetzbar bleibt, was in imperativen Sprachen nicht gilt.
• Property-Based Testing ist der erste praktische Schritt zu formalen Methoden: Man formuliert Eigenschaften mit Allquantoren über alle Eingaben statt nur einzelne Beispiele zu prüfen, und das funktioniert in allen gängigen Programmiersprachen.
• C und C++ gelten als die gefährlichsten Programmiersprachen, werden aber ausgerechnet in sicherheitskritischen Embedded-Systemen wie Autos und Medizingeräten eingesetzt, wo formale Methoden zumindest grundlegende Korrektheitseigenschaften absichern können.

Was sind formale Methoden in der Softwareentwicklung?

Formale Methoden sind ein Oberbegriff für mathematisch fundierte Techniken, mit denen sich Entwickler bestimmter Eigenschaften ihrer Software überzeugen. Der Name kommt vom Formalisieren, also vom Übersetzen einer Anforderung in mathematische Form.

Im Kern geht es um einen Beweis statt um Stichproben. Beim klassischen Testen liegt zwar eine Spezifikation vor, oft ergänzt durch eine Handvoll Beispiele. Diese Beispiele beantworten die Frage, was in genau diesen Fällen passiert. Sie sagen nichts darüber, was überall sonst passiert.

Michael Sperber beschreibt das am Beispiel eines Tachometers. Ein Auto fährt mit einer bestimmten Geschwindigkeit, und der Tacho soll das reale Tempo anzeigen. Für diese Anforderung existiert eine EU-Norm, die eine Formel vorgibt: Bei einem gegebenen Tempo darf die Anzeige nur um einen bestimmten Anteil abweichen. Eine Zertifizierungsbehörde will sich davon nicht mit sieben Beispielen überzeugen lassen, sondern mit einem allgemeinen Argument.

Formale Methoden liefern dieses Argument. Aus der Norm-Formel wird eine mathematische Aussage, der Code wird ebenfalls in mathematische Form übersetzt, und ein Beweis zeigt, dass beide zusammenpassen.

Korrektheit ist kein Endpunkt, sondern eingebaute Redundanz

Die Frage, ob Software danach “wirklich richtig” ist, gehört eigentlich ans Ende. Sperber dreht sie um und betrachtet formale Methoden aus der Sicht eines Ingenieurs.

In jeder Ingenieursdisziplin baut man Redundanz ein, um ein System verlässlich zu machen. Formale Methoden sind ein Mittel, diese Redundanz massiv zu steigern. Die Absicherung wird so dicht, dass kaum noch ein Fehler durchkommt.

In der Praxis nennen es die Beteiligten “bombensicher” oder “kugelsicher”. Aus der vorsichtigeren Ingenieursperspektive lautet die Aussage präziser: Es ist die zuverlässigste bekannte Methode, um sich von Eigenschaften der Software zu überzeugen, und sie reicht um ein Vielfaches weiter als das, was Tests allein erreichen.

Warum funktionale Programmierung näher an der Mathematik liegt

Formale Methoden setzen einen Beweis voraus, und Beweise leben von Gleichungen. Genau hier trennt sich funktionale von imperativer Programmierung.

In C oder Java ist x = x + 1 ein vertrauter Ausdruck. Mathematisch ist er falsch, denn x ist nicht dasselbe wie x + 1. Der Ausdruck funktioniert nur als Anweisung: x neu ist x alt plus eins. Zwischen diesem Programmiermodell und der Mathematik klafft eine Lücke.

Diese Lücke lässt sich überbrücken, aber das kostet Arbeit. Wer ein C- oder Java-Programm verifizieren will, hat es zusätzlich mit Pointern zu tun, die auf gemeinsamen Zustand zeigen. Eine Änderung an einer Stelle kann eine andere Stelle beeinflussen. In der Mathematik gilt dagegen: Steht x für 5, lässt sich überall 5 einsetzen. Gleiches durch Gleiches ersetzen. In imperativem Code gilt das nicht, und es braucht viel Maschinerie, um es wiederherzustellen.

In funktionaler Programmierung stellt sich das Problem nicht. Wer eine Funktion definiert, schreibt im Kern eine Gleichung. Damit ist man schon nah an mathematischen Schlussweisen und an dem, was ein Beweis braucht.

Markus Schlegel ergänzt einen zweiten Blick: Funktionale Programmierung beschreibt, was ist, also die fachlichen Zusammenhänge. Imperative Sprachen wie C beschreiben, wie der Computer etwas Schritt für Schritt tun soll. Eine korrekte Geschwindigkeitsmessung im Pkw lässt sich funktional als Eigenschaft formulieren, nicht als Reihenfolge von Anweisungen.

Funktionale Programmierung kostet nicht mehr, sondern oft weniger

Der Verzicht auf vertraute imperative Konstrukte wirkt zunächst wie eine Askese. In der Praxis ist funktionale Entwicklung jedoch nicht aufwendiger, sondern häufig effizienter.

Ein Grund liegt in zusätzlichen Abstraktionsmöglichkeiten, besonders in der Datenmodellierung. Der andere Grund ist die einfachere Argumentation über das Verhalten des Programms. Über Input und Output nachzudenken ist überschaubarer, als jeden Zustandsschritt in der richtigen Reihenfolge im Kopf zu halten.

Ich debugge gar nicht so viel in der funktionalen Programmierung. Ich gucke eben nach, wie liefert mir meine Funktion die richtigen Ergebnisse für die entsprechenden Inputs. Michael Sperber

Untersuchungen zum Aufwand pro Stück Funktionalität fallen laut Sperber durchweg zugunsten der funktionalen Entwicklung aus. Über den genauen Faktor lässt sich streiten, eine Einbuße entsteht nicht.

Wer aus der Uni und der imperativen Schule kommt, muss dafür umdenken. Schlegel beschreibt i = i + 1 als ersten Stolperstein seines Programmierenlernens, weil es dem widersprach, was er aus der Schulmathematik kannte. Der Weg zu formalen Methoden führt ein Stück weit zurück zu diesem Gleichungsdenken.

Funktionale Sprachen sind ein eigenes Ökosystem, keine Einzelsprache

Funktionale Programmierung existiert nicht als eine Sprache, sondern als paralleles Ökosystem mit eigenen Sprachen, Package-Managern und Frameworks. Es hat sich weitgehend unabhängig vom Mainstream entwickelt.

• Haskell gilt als prototypischer Vertreter mit starkem Typsystem.
• Scala auf der JVM.
• F# auf der .NET-Plattform, sozusagen die funktionale Parallelwelt zu C#.
• Clojure auf der Java-Plattform.

Das starke Typsystem in Haskell ist Absicht: Wer etwas tendenziell Falsches programmiert, bekommt das Programm gar nicht erst kompiliert. Diese Strenge schreckt manche ab. Schlegel weist darauf hin, dass man nicht zwangsläufig Haskell mit seinen Monaden und Monoiden braucht. Clojure ist ebenfalls funktional, ohne diese Hürden in den Vordergrund zu stellen.

Viele Features moderner objektorientierter Sprachen stammen ohnehin aus der funktionalen Programmierung. Was dort entlehnt wird, war im funktionalen Lager schon länger vorhanden.

Wie ein Beweis im Code entsteht und überprüft wird

Ein Beweis lässt sich auf Papier, am Whiteboard oder maschinell führen. Für formale Methoden zählt am Ende die maschinelle Überprüfung.

Der einfachste Einstieg sind Typsysteme. Ein Compiler beweist bereits, dass sich ein Programm auf bestimmte Arten verhält, etwa dass kein Integer dort steht, wo ein String erwartet wird. Neuere funktionale Sprachen kennen sogenannte Dependent Types. Damit lässt sich mehr von einer Spezifikation direkt als Typ ausdrücken, und der Typchecker verifiziert sie.

Der zweite Weg sind Beweisassistenten. Sie führen einen Beweis wie in der Schule, nur mit Werkzeugunterstützung. Man schreibt einen Beweis maschinenlesbar auf und lässt prüfen, ob er gilt. Moderne Tools nehmen die nervigen Teile ab. Wer dem Assistenten sagt, er solle eine Induktion über eine Variable führen, kann die einzelnen Schritte vom Tool elaborieren lassen.

Als ausgereiftes Beispiel nennen die beiden Isabelle, ein Tool, das zur Hälfte aus München stammt und seit vielen Jahren produktiv nutzbar ist.

Die Sicherheit entsteht durch das System selbst. In einer Sprache mit starkem Typsystem kompiliert das Programm nicht, solange der Beweis nicht korrekt ist. Schlegel fasst das Prinzip einfach: Wenn am Ende die Lampe grün wird, stimmt der Beweis, und Spezifikation und Implementierung sind in Einklang.

Beweise gehören in die CI wie Tests

Ein fertiger Beweis ist Code und wird wie Code behandelt. Mal liegt er in einer separaten Datei, mal ist er bei Dependent Types direkt in den Quellcode integriert.

Damit lässt er sich ablegen und in die Continuous Integration einbauen. Statt nur eine Testsuite durchlaufen zu lassen, läuft zusätzlich der Beweischecker über das Programm und meldet, falls etwas nicht stimmt. Der Beweis wird so zu einem regulären Bestandteil der Pipeline, nicht zu einer einmaligen Sonderaktion.

Formale Methoden sind eine Nische, gehören aber nicht in eine

Formale Methoden gelten als Nische, obwohl sie für nahezu jeden Bereich taugen. Auf die häufige Frage, wofür sich der Ansatz eigne, antwortet Sperber: für alles. Die guten Eigenschaften funktionaler Programmierung bieten überall Vorteile.

Im Embedded-Umfeld bleibt die Realität anders. Dort dominieren C und C++, also die gefährlichsten Sprachen für Systeme, die zuverlässig funktionieren sollen, etwa in einem Auto oder einem Medizingerät. Hier setzen formale Methoden noch unterhalb der funktionalen Korrektheit an. Sie prüfen, ob ein Programm Ressourcen begrenzt verbraucht, ob Pointer-Aliasing sauber bleibt und ob das C-Programm überhaupt wohldefiniertes Verhalten zeigt.

Ein praktikabler Pfad sieht so aus: Die Software wird funktional entwickelt, getestet und verifiziert, und erst danach wird C-Code generiert. Der generierte Code bewegt sich dann in engen, definierten Schranken.

Formale Methoden gibt es seit den 1950er-Jahren. Die Tools sind entsprechend gereift. Was im Mainstream fehlt, ist oft schlicht das Wissen, dass es das alles gibt.

Drei Lifehacks, mit denen du sofort anfangen kannst

Der Einstieg in formale Methoden braucht keinen Beweisassistenten am ersten Tag. Drei Schritte funktionieren in jedem Kontext.

Erstens: die Spezifikation aufschreiben. Wer Testfälle formuliert, zieht sie nicht aus dem Hut, sondern aus einer Vorstellung davon, wie das Programm funktionieren soll. Diese Vorstellung explizit aufzuschreiben ist der erste Schritt und hilft unabhängig von der eingesetzten Technik.

Zweitens: Property-Based Testing nutzen. Diese Technik stammt aus der funktionalen Programmierung, ist aber für alle gängigen Sprachen verfügbar. Statt einzelner Beispiele formuliert man Eigenschaften über alle möglichen Eingaben, etwa mit einem Allquantor. Das ist noch nicht kugelsicher, weil die Tests generiert und nicht bewiesen werden. Es ist aber ein echter Schritt in Richtung formaler Spezifikation.

Schlegel und Sperber stellen fest, dass Property-Based Testing in der Tester-Community kaum bekannt ist, obwohl es eine originäre Testtechnologie ist.

Drittens: funktional denken lernen. Über das Verhältnis von Input und Output nachzudenken statt über Reihenfolgen von Anweisungen reduziert Fehler bereits in der Entwicklung. Material dazu gibt es frei verfügbar, und das ISAQB hat ein neues Curriculum zu formalen Methoden ausgearbeitet, das einen Überblick über das Feld gibt.