Software testen bedeutet meist: ein paar Beispiele ausprobieren und hoffen, dass der Rest auch funktioniert. Formale Methoden gehen einen radikal anderen Weg – sie beweisen mathematisch, dass Code für alle denkbaren Fälle korrekt ist. Funktionale Programmierung bildet dabei die Brücke zwischen Mathematik und Code, weil sie mit Gleichungen statt mit Zustandsänderungen arbeitet. Property Based Testing ist der erste praktische Einstieg in diese Welt, bevor man zu Beweisassistenten greift.
In dieser Episode spreche ich mit Michael Sperber und Markus Schlegel über formale Methoden – die vielleicht unbekannteste und gleichzeitig mächtigste Technik, um Software wirklich korrekt zu machen. Während wir beim Testen oft nur ein paar Beispiele prüfen, ermöglichen formale Methoden Software mathematisch zu beweisen, dass sie für alle möglichen Eingaben das Richtige tut. Die beiden zeigen, warum funktionale Programmierung der Schlüssel dazu ist, wie Property Based Testing der erste praktische Schritt sein kann und weshalb dieser Ansatz nicht nur sicherer, sondern oft sogar effizienter ist als klassische Entwicklung.
„C und C++ sind die gefährlichsten Programmiersprachen auf der Welt, ausgerechnet für die Systeme, von denen wir wollen, dass die richtig funktionieren." - Michael Sperber
Dr. Michael Sperber ist Geschäftsführer der Active Group GmbH, die Individualsoftware ausschließlich mit funktionaler Programmierung entwickelt. Er ist international anerkannter Experte für funktionale Programmierung und wendet sie seit über 20 Jahren in Forschung, Lehre und industrieller Entwicklung an. Außerdem hat er zahlreiche Fachartikel und Bücher zum Thema verfasst, sowie das Curriculum für das iSAQB-Advanced-Modul "Formale Methoden" (zusammen mit Lars Hupel). Michael Sperber ist Mitbegründer des Blogs funktionale-programmierung.de und Mitorganisator der Entwicklerkonferenz BOB.
Markus Schlegel ist Softwarearchitekt bei der Active Group GmbH. Markus hat 2013 die funktionale Programmierung für sich entdeckt und schläft seither wieder ruhig.
Formale Methoden klingt erst mal kompliziert. Es weckt Bilder von Gleichungen und Beweisen aus der Schulzeit. Doch worum geht es wirklich? Michael Sperber erklärt, dass formale Methoden mathematisch fundierte Techniken sind, die uns helfen, bestimmte Eigenschaften von Software sicher nachzuweisen. Konkretes Beispiel: Ein Tacho im Auto muss möglichst immer richtig anzeigen. Es reicht nicht, den Tacho mit ein paar Testfahrten zu prüfen. Die EU will garantieren, dass bei allen Geschwindigkeiten die Abweichung innerhalb vorgeschriebener Grenzen bleibt. Solche Anforderungen lassen sich als mathematische Gleichungen formulieren und können mit formalen Methoden überprüft werden.
Statt also nur einzelne Beispiele durchzutesten, beschreibt man genau, was die Software immer erfüllen muss. Danach übersetzt man die Software und die Vorgaben in die Mathematik und überprüft, ob sie wirklich zusammenpassen. So entstehen echte Beweise dafür, dass etwas stimmt.
Formale Methoden bauen oft auf funktionaler Programmierung auf. Aber was ist das eigentlich? In Sprachen wie C oder Java erzählen wir dem Computer genau, wie er etwas tun soll. Wir sagen nicht einfach "das Ergebnis ist so", sondern geben eine genaue Schritt-für-Schritt-Anweisung. Das macht es schwierig, mathematisch exakt zu argumentieren.
Anders bei funktionaler Programmierung: Hier beschreibt man eher, "was ist". Funktionen sind wie Gleichungen in der Mathematik. Wenn die Funktion stimmt, stimmt der ganze Zusammenhang. Markus Schlegel meint, dass damit die Fachlichkeit, also das, was die Software tun soll, sofort klar im Code steht – ohne dass man Kommentare oder extra Dokumentation braucht.
Programme in funktionalen Sprachen wie Haskell, F#, Scala oder Clojure erlauben es sogar, viele Eigenschaften und Regeln direkt auszudrücken und später mathematisch zu beweisen. Man arbeitet also näher an den mathematischen Methoden und kann besser prüfen, ob alles korrekt läuft.
Eine Software zu beweisen klingt riesig und kompliziert. Muss man da wochenlang rechnen? Laut Michael Sperber bedeutet es zwar etwas Umdenken, ist aber oft nicht aufwendiger als klassisches Testen. Vor allem helfen dabei spezielle Tools weiter – sogenannte Beweisassistenten. Sie unterstützen dabei, die Beweisführung zuverlässig und sogar ein Stück automatisiert umzusetzen.
Der Beweis selbst wird meistens im Code hinterlegt oder in extra Dateien abgelegt. Die Tools prüfen dann bei jedem Software-Build, ob die Beweise noch gelten – ganz so wie übliche Tests.
Bevor man sich an ganze Beweise heranwagt, gibt es einen guten Zwischenschritt: Property-Based Testing. Diese Methode kommt aus der funktionalen Programmierung und hat inzwischen auch Einzug in viele andere Sprachen gehalten. Die Idee: Man beschreibt Eigenschaften ("Properties"), die immer gelten sollen, für alle möglichen Eingabedaten. Das Test-Tool erzeugt dann automatisch viele verschiedene Tests und prüft, ob die Software sich wie beschrieben verhält.
So kann man schon ohne vollständigen Beweis viele Programmfehler finden, und sich an die Denkweise der formalen Methoden gewöhnen.
Die Meisten testen aktuell "nur" durch Beispiel und hoffen, dass der Code dann in allen Fällen richtig läuft. Doch wie Richie im Gespräch sagt, reichen diese Methoden bei komplexen und sicherheitskritischen Systemen längst nicht mehr aus. Deshalb nutzen zum Beispiel Firmen im Automotive- oder Medizinbereich vermehrt formale Methoden – und es lohnt sich für alle, mal genauer hinzuschauen.
Wer neugierig geworden ist, findet auf deinprogramm.de einen von Michael Sperber entwickelten, frei verfügbaren Einstieg ins Thema. Auch der ISAQB hat dazu ein Curriculum veröffentlicht. Einfache Methoden wie Property-Based Testing kann man direkt ausprobieren.
Formale Methoden sind nicht nur für Freaks oder Forscher, sondern für alle, die robuste Software entwickeln wollen. Sie helfen, Software-Qualität auf ein neues, messbares Niveau zu heben – und machen den Alltag für Entwickler und Tester leichter und sicherer. Wer einmal erlebt hat, wie es sich anfühlt, eine Sicherheit zu belegen statt nur zu hoffen, versteht den Wert dahinter. Es lohnt sich, genauer hinzuschauen!