Happy Quality, es ist wieder World Quality Week und da wollen wir Softwarequalität wieder mal so richtig abfeiern. Drum gibt es in dieser Woche wieder jeden Tag eine Spezialfolge zum Thema Testen Qualität und was sonst noch dazu gehört. Also lasst uns Software besser machen. Viel Spaß! Hallo und herzlich willkommen zu einer neuen Folge vom Podcast Software Testing. Ich bin euer Host Ritchie und habe eine Folge von den Software Quality Days 2024 aus Wien mit dabei.
Eine Grundaussage über das Testen ist ja, dass wir keine Fehlerfreiheit garantieren können. Was aber, wenn man Fehlerfreiheit korrekt beweisen muss? Wie kann man da hinkommen? Da können formale Methoden helfen. Eine ganz eigene Disziplin in der Qualitätssicherung. Wie das funktioniert und welche Tools es dafür gibt, darüber habe ich mit Bianca und Lars gesprochen. Und jetzt viel Spaß beim Beweisen, äh beim Hören. Hallo Bianca, hallo Lars, schön, dass ihr da seid. Hallöchen.
Danke, dass wir hier sein dürfen. Ja, ganz schön. Wir haben den zweiten Tag von den Software Quality Days hier in Wien. Ihr habt euren Vortrag noch vor euch. Genau, vorletzter Slot. Krönender Abschluss. Das Beste kommt zum Schluss. Hoffentlich. Hoffentlich kommen auch die Leute zum besten Abschluss dann. Aber ihr könnt euch jetzt hier schon ein bisschen warm quatschen. Das ist ja auch ganz gut.
Ja, ich habe im Vorfeld die Abstracts und die Speakerliste gescreent und da bin ich so bei euch am Vortrag auch hängen geblieben. Weil es darum geht, so um diese quasi formale Sicht auf Software. Wie kann das formal korrekt sein? Dann haben wir gedacht, oh, spannendes Thema. Und da wollen wir uns mal ein bisschen drüber unterhalten. Ja, gerne. Fangen wir gleich mal an. Was heißt denn das und warum brauche ich denn das überhaupt? Lars? Ja, ich kann gerne einsteigen. Steig rein.
Ich bin ja aktuell bei einer Firma, die unter anderem Finanzprodukte herstellt, also Software für Zahlungssysteme. Und ich sage mal im Allgemeinen, Bankkundinnen, die mögen das nicht so gerne, wenn Geld verloren geht bei einer Transaktion. Kann ich mir gar nicht vorstellen. Und es gibt halt bestimmte Anforderungen. Das ist jetzt nicht nur bei uns in der Finanzbranche. Man kann ja auch mal an Automotive denken.
Oder an Medizin. Wo es halt wirklich so ist, dass, wenn da was schiefläuft, dann rollen Köpfe. Das heißt, da muss man wirklich sehr, sehr, sehr stark sich anstrengen, dass das wirklich alles korrekt ist. Und es gibt eben bestimmte Eigenschaften, die kann ich durch Testen nicht erreichen. Also wenn wir zum Beispiel bei uns sagen, für jede mögliche Konstellation einer Transaktion darf das Geld nicht verloren gehen.
Zum Beispiel, mal ganz konkret, ich habe eine Zahlungskarte und halte die per NFC dran. Und dann rutscht da irgendwie die ab oder ich habe irgendwie einen Verbindungsverlust. Egal wann das passiert. Ich muss immer in der Lage sein, die Transaktion zurückzurollen und nochmal über neu zu versuchen. Und das ist halt etwas, was ich mit Testen nicht erreichen kann, weil da habe ich immer nur Beispiele.
Kann ich mir nur auflisten. Fall 1, Fall 2, Fall 3. Vielleicht noch Fall 4, Fall 5, wenn ich mir Mühe geben will. Aber was wir im Prinzip brauchen in unserem Produkt ist: Für alle. Genau. Eine Garantie dafür, dass es den Worst Case gar nicht geben kann. Also dass es uns nicht durchrutschen kann beim Testen. Also man denke an Dykes damit. Mit Tests kann ich Fehlerfreiheit nicht nachweisen. Es gibt einfach bestimmte Domänen, da brauche ich aber die Fehlerfreiheit.
Und eben auch den Nachweis. Und da kommen genau formale Methoden zum Tragen. Wo ich in tatsächlich mathematisch rigoroser Art und Weise über meine Software nachdenke, über meine Software spreche, die sehr strikt modelliere und dann eben in der Lage bin, Eigenschaften dieser Softwareinvarianten auch auf diesem formalen Level so zu formulieren, dass ich sie halt, dass ich eben tatsächlich Aussagen für alle möglichen Eingaben und Ausgaben formulieren kann.
Und dann mit Hilfe des Computers halt verifizieren, dass diese Beweise, die Gründe, warum ich sage, die Eigenschaften gelten, dass die tatsächlich stimmen, dass die tatsächlich keine Lücken enthalten, dass ich da nicht falsche Schlüsse drin habe.
Und das ist genau was der Computer dann, wenn man in wirklich so Beweisassistenten, also so das, wo ich wirklich einen mathematisch komplexen Beweis über ein komplexes System fahre, dann halt vom Computer erreiche, dass der mir nachweist: Okay, ja, du hast da auch nichts weggelassen. Mhm. Wie kann ich mir denn das in der Praxis vorstellen? Also beim Testen, das ist für mich klar, ich habe irgendwann mal die Software und dann meine Testfälle und die klicke ich durch.
Wo setzt ihr denn im Prozess an, in dem ganzen Entwicklungsprozess mit den Themen und wie sieht das dann so in der Praxis aus? Da hast du gleich die schwierigste Frage zum Anfang gestellt. Ja, natürlich. Aber da war ja keine Zeit für das. Um mal ein Beispiel zu nennen, wir nennen das auch in unserem Vortrag das Beispiel, es gibt einen verifizierten Mikro-Kernel, der heißt SCL4.
Das ist also ein Mikro-Kernel, Betriebssystem-Kernel, der wird viel in Embedded Systems benutzt, also zum Beispiel Drohnen, oder irgendwelche anderen Maschinen, Geräte. Und der wurde komplett verifiziert mit einer Software, die nennt sich Isabell. Und man hat dort ungefähr so geschätzt, also das ist wirklich ganz, ganz grobe Schätzung, dass man ungefähr einen Overhead von so, je nachdem, was man für eine Programmiersprache hat, 10 bis 100 hat.
Das heißt, nehmen wir jetzt einfach mal 10, das klingt nicht ganz so schlimm, also jede Zeile Code erfordert 10 Zeilen Beweis. Mhm. Das ist also schon mal eine sehr schwierige Sache, das in der Praxis mal zu bringen, weil dann muss ich nämlich zu meinem Chef, meiner Chefin gehen und sagen, du, ich brauche eigentlich noch für dieses Feature, was zwei Monate gedauert hat, brauche ich noch zwei Jahre, um das zu validieren. Das kommt halt dann ganz darauf an, wo dann der Leidensdruck da ist.
Aber es muss auch gar nicht so schlimm sein, weil es gibt da auch Abstufungen, also es gibt auch viel leichtgewichtigere Prozesse. Und ich würde mal sagen, der leichtgewichtigste Prozess, der leichtgewichtigste formale Methode, die wahrscheinlich die meisten von deinen Hörer*innen schon mal benutzt haben, sind Typsysteme.
Also Typsysteme sind auch eine Form von sehr leichtgewichtigen formalen Methoden, weil der Typchecker schon mal sagt, okay, ich weiß zwar nicht, was es für ein Wert ist, aber ich kann dir mal mit Sicherheit sagen, dass es ein String ist und keine Zahl. Für alle Aufrufe von dieser Funktion ist es immer ein String. Das heißt, wenn du nur die String-Methoden benutzt, dann bist du schon mal safe, schon mal ein Basislevel. Und da kann man halt zwischen diesen Extremen sehr viel Schattierungen machen.
Ja, in Bezug auf Ausdrucksmächtigkeit. Also so ein Typchecker, der sagt mir halt nicht viel über meine Software. Das ist wieder, ich muss nicht viel investieren, der läuft einfach mit. Ich habe das Ergebnis quasi umsonst, aber dafür ist das Ergebnis auch nicht sehr aussagekräftig in Bezug auf Korrektheit zum Beispiel. Also wenn ich über Korrektheit spreche, dann muss ich schon ein bisschen mehr in die Semantik meines Systems gehen.
Aber auch da gibt es eben Abstufungen wie Modelchecker ist vielleicht dem einen oder anderen ein Begriff, wo ich halt mein System sehr abstrakt fasse, sehr abstrakt modelliere und dann auch noch mit einem sehr hohen Maß an Autoregulierung. Und dann kann ich halt auch mit einer Automatisierung halt bestimmte Eigenschaften prüfen, wo man der Computer eben tatsächlich sagt, gibt es da einen Pfad, den ich als nicht erlaubt definiert habe, den meine Software noch gehen kann?
Also finde ich ein Gegenbeispiel oder folgt meine Software meinen Vorgaben? Ich glaube, ein wichtiger Punkt, um überhaupt darüber nachzudenken, wie funktioniert Formalisierung, wie kann ich das in der Praxis verwenden, ist, dass man das sich nicht vorstellen kann, wie ich schreibe hier mal meine Binary, mein Programm. Und dann schmeiße ich das über den Zaun zu Leuten wie Lars und mir und sage, jetzt zeigst du mal, dass das alles passt. Sondern gerade bei SEL4 sieht man das gut.
Das ist ein Punkt, den ich eigentlich bei der Entwicklung schon ein bisschen mitdenken muss und mitdenken will, weil es auch den Entwicklungsprozess bereichert. Also in dem Augenblick, wo ich gleich bei der Entwicklung schon jemanden habe, der abstrakter über die Domäne nachdenkt, abstrakter über das System nachdenkt, dann kriege ich von dem auch gegebenenfalls schon frühzeitig Input über interessante Systemeigenschaften.
Und halt einfach das Feedback so, lass uns mal vielleicht auf diese Sonderlocke verzichten, weil wir die eigentlich nicht in den Griff kriegen in so einem allgemeinen Fall und dann bestimmte Garantien verlieren. Und wenn ich das ziemlich am Anfang mitdenke, dann habe ich eine Chance, irgendwo dahin zu kommen, dass ich ein sehr, also sowohl funktional ausgereiftes System kriege, wie eines, was sich diesem Beweis zugänglich hält. Verstehe. Wenn ich so ein Model generiere draus. Oder mache drauf.
Also wenn ich das automatisiert mache aus einem System heraus, dann weiß ich, okay, das ist das, was die Software vielleicht darstellt. Aber manuell hätte ich ja da wieder schon eine Fehlerprächtigkeit, dann würde das ja keine Aussage dann bringen. Genau, also es gibt sowohl automatische als auch manuelle Methoden und auch alle Chartierungen dazwischen. Also es gibt nicht das eine Verifizierungsdruck, sondern es gibt da zig verschiedene.
Um mal ein konkretes Beispiel zu nehmen für etwas, was sehr automatisiert stattfindet. Seit Windows 7, glaube ich, oder spätestens seit Windows 10, prüft Microsoft sämtliche Treiber, die man als Gerätehersteller mitliefern möchte mit Windows, auf bestimmte Korrektheitseigenschaften. Zum Beispiel soll der Treiber möglichst keine Endlosschleifen produzieren. Das wäre irgendwie schlecht. Keine Nullpointer haben und solche Sachen. Das ist mittlerweile sehr gut verstanden.
Also die Treiber, die werden dann im C-Code, also der Hersteller muss dann C oder C++-Code zu Microsoft schicken. Also die Details kenne ich jetzt auch nicht. Das, was halt öffentlich bekannt ist über den Prozess. Man schmeißt dann da im Prinzip diesen Code rüber und dann gibt es da automatisierte Tools, sozusagen Static Analysis on Steroids. Was da drüber läuft und zum Beispiel guckt, dass da keine Endlosschleifen drin sind. Und manchmal muss man diesen Tools ein bisschen helfen.
Ein konkretes Beispiel, wenn ich jetzt irgendeine nicht triviale Schleife habe, irgendeine Y-Schleife, dann kann es sein, dass ich da irgendeinen Kommentar drüber schreiben muss, der dann maschinenlesbar ist, wo dann zum Beispiel drinsteht, du pass mal auf, in jedem Durchlauf von dieser Schleife wird jetzt hier irgendwie ein Counter verringert.
Und dann weiß das Tool, aha, okay, ich brauche bloß gucken, ob der Counter... ...sich immer verringert und wenn er dann irgendwann bei null ist, ist er fertig. Also das sind dann so halb automatische bis automatische Dinge. Und das ist dann wirklich sehr, sehr nah am Code. Das heißt, das ist dann wirklich der Code, der auch ausgeführt wird. Das ist sozusagen das, was man sich so vorstellt. Das ist eigentlich der Goldstandard. Tatsächlich der Code, der ausgeführt wird, wird auch verifiziert.
Das Problem ist, das ist halt sehr aufwendig und ja, nicht jeder hat da irgendwie Zeit dafür zu machen. Und man kann auch bei weitem nicht alle Eigenschaften damit beweisen. Zum Beispiel habe ich dann immer noch nicht bewiesen, dass der Treiber auch das macht, was er soll. Ich habe halt nur bewiesen, dass er nicht crasht. Und dann, wenn man so ein bisschen mehr in die manuelle Ecke geht, dann könnte man sagen: Okay, ich schreibe mir jetzt ein Modell auf.
Das wäre dann zum Beispiel ein abstrakter Algorithmus. Also ich weiß zum Beispiel, mein Code soll jetzt irgendwie oder mein Tool soll auf der sehr hohen Ebene folgende Spezifikationen erfüllen und keine Ahnung, es soll irgendeine Zahl rauskommen. Die Zahl muss sich im Bereich von 10 bis 100 bewegen. Mal ganz, ganz hypothetisch gesagt. Dann implementiere ich das vielleicht in so einem formalen Tool. Und dann ist es aber vielleicht nicht mein richtiger Code.
Und dann kann man sich halt die Frage stellen: Ist das schon hilfreich? Meistens ja, weil meistens fangen die Fehler schon in der Spezifikation an. Also man kennt das. Also man redet mit jemandem, sagt: Ah, die User Story ist irgendwie ganz einfach. Und dann denkt man darüber nach: Was ist da jetzt eigentlich gemeint? Und was kommt da jetzt eigentlich in diesen Grenzfällen raus? Und dann kann es natürlich immer noch passieren, dass dann die Implementierung sich nicht so verhält wie das Modell.
Aber zumindest habe ich schon mal in meiner Gedankenwelt das einigermaßen gut beschrieben. Und dann die ganz entfernteste Ebene wäre dann einfach mal, überhaupt eine Spezifikation aufzuschreiben, vielleicht in Englisch oder auf Deutsch oder wie auch immer. Und dann zu sagen: Vielleicht schreibe ich mal ein paar Formeln rein, mal was ganz Neues in die User Story.
Schreibe ich halt irgendwie rein, ja, irgendwie, keine Ahnung, ich habe irgendwie ein Navi und dann ist halt eine Formel drin, dass, keine Ahnung, irgendwie der Abstand zwischen Start und Endpunkt irgendwie so und so sein muss oder irgendwie sowas. Das wäre dann so das ganz Informelle sozusagen. Und man muss halt immer dann gucken: Was ist denn für meinen Anwendungsfall relevant? Und wie viel bin ich Willens, denn da zu investieren? Aber ich sage immer mal so: Es ist so ähnlich wie Tests.
Also man kann ja bei Tests auch sagen: Ich kann jetzt irgendwie super viel Aufwand in 100% Coverage stecken. Vielleicht brauche ich das aber auch gar nicht. Vielleicht kann ich, reicht es auch, wenn ich 80% Coverage habe und 80% ist schon besser als 0. Und Test ist ein gutes Stichwort. Also ich finde es immer wichtig, im Kopf zu behalten, dass formale Methoden auch nicht die Silver Bullet und Heilmittel sind. Das finde ich formale Methoden, da muss ich nichts mehr anderes und alles ist bewiesen.
Und schön, so funktioniert es nicht. Also es ist eine sehr wichtige Bereicherung, um mein System besser zu verstehen, eben auf eine Spezifikation zu kommen, mit der man arbeiten kann. Und dann kann ich aber natürlich auch noch testen. Also ich habe, wir haben ein weiteres Beispiel, was wir in unserem Vortrag haben, ist ComSare. Das ist ein C-Compiler, der verifiziert ist. Und die haben den Compiler-Kern an sich verifiziert.
Aber da, wo der C-Code reingeht und wo dann der echte Maschinencode rausgeht, das ist halt nicht formalisiert und nicht verifiziert. Und jetzt kann man argumentieren, ja woher weiß ich denn, dass diese initiale Übersetzung schon funktioniert? Oder nicht hinten raus Fehler entstehen. Und da kann man dann eben so mit Compiler-Fuzzing, so Fuzzy-Testing, halt Tools draufschmeißen, die da ja randomisierte C-Programme durchschmeißen.
Und wenn, das gibt es ein Paper, wo die das sehr, also auf Herz und Nieren genau auf diese Art und Weise geprüft haben. Und dann kann man noch mal ein bisschen mehr Sicherheit bekommen dafür, dass es auch an diesen, an den Randfällen, an den Rändern halt immer noch passt. Oder ich nehme eine zweite andere Implementierung und stelle die als Referenzimplementierung daneben und sage, okay, ich gucke mir mal das Verhalten an. Ja. Deckt sich das?
Also solche Methoden sind nach wie vor ja zur Verfügung und sollte man dann auch genau noch daneben stellen, um sich wirklich abzusichern. Also ich, unser Titel ist kugelsichere Architektur. Und das ist so ein bisschen, ist ein bisschen dick aufgetragen, weil das ist nicht, das ist nicht eben nicht kugelsicher. Also das ist nicht der World, wo gar nichts mehr passieren kann. Aber ich. Aber die kugelsicheren Westen sind ja auch nicht unbedingt kugelsicher.
Wenn ich woanders treffe, wo ich keine Weste trage, dann habe ich halt auch ein Problem. Ungefähr so ist es gedacht. Also mein Kopf ist nach wie vor nicht geschützt, aber mein ganzer Torso, also eine sehr große Fläche ist abgedeckt. Und damit bin ich schon sicherer und habe mehr, mehr Sicherheit als ohne das. Einen Punkt wollte ich noch mal kurz erwähnen, weil du es auch erwähnt hattest. Und zwar dieses zwei Implementierungen nebeneinander stellen. Es gibt dieses schöne Zitat.
Ich habe leider vergessen von wem. Wenn man etwas implementiert, hat man zwei Möglichkeiten. Man macht es so. Einfach, dass es offensichtlich keine Fehler gibt. Oder man macht es so komplex, dass es keine offensichtlichen Fehler gibt. Und meistens braucht man die komplexe Implementation, weil man Performance oder sonst irgendwelche anderen Anforderungen hat. Und es ist ja kein Problem, wenn man noch eine einfache Implementierung daneben stellen kann, die vielleicht super, super unperformant ist.
Und man vergleicht die dann einfach miteinander. Dann hat man halt den Testlauf, der dauert dann halt vielleicht eine Stunde oder so. Who cares? Solange dann meine performante Implementierung korrekt ist, bin ich willens, diesen Preis dann zu bezahlen. Jetzt klingt der formale Nachweis oder auch in dem Umfeld, wo das passiert, da geht es ja dann auch ein bisschen Richtung Safety, Richtung Regulatorik und sowas.
Wie sieht es denn da aus mit dieser Beweisführung, wie die auch dokumentiert und niedergeschrieben wird? Gibt es da Vorgaben, wie sowas passieren muss? Oder ist das quasi dann einfach ein wissenschaftlicher Report sozusagen, wo dann darunter steht: Ich habe bewiesen. Punkt. Also auch da gibt es Schattierungen. Mir wäre jetzt keine Richtung. Ich habe ja auch keine Regulierung bekannt, wo wirklich ein konkretes Tool drinsteht. Eine Sache sind diese Common Criteria Level.
Es gibt in Common Criteria diese Level 1 bis 7, glaube ich, ist das. Und da ist irgendwie Level 3 ist irgendwie so vernünftig getestet und Level 4 ist dann irgendwie getestet mit Extrasachen. Also ich habe eigentlich gar keine Ahnung. Man hört wahrscheinlich, dass ich keine Ahnung davon habe. Aber Level 7 ist dann wirklich formal verifiziert. Und da ist es dann aber wirklich nicht relevant, welche Tools man benutzt. Also ich kann das zum Beispiel mit Isabel machen, was SEL4 benutzt hat.
Aber solange da irgendwie eine Tool-Unterstützung drin ist und solange man das irgendwie wissenschaftlich, Stand der Technik sozusagen, verargumentieren kann, wird da keine regulatorische Organisation sagen: Nee, das hast du jetzt leider mit dem falschen Tool gemacht. Also ich glaube, es gibt da eine ganze Reihe von bekannten Tools, die für solche Projekte eingesetzt werden. So Model Checking ist da auch sehr oft mit drin. Aber mir wäre jetzt nicht bekannt.
Ja. Also die Tools unterscheiden sich dann auch. Die unterscheiden sich da halt auch stark. Das ist meist, also oftmals ist das dann einfach, sieht auch wie Source Code aus. Also man hat dann da zum Beispiel irgendwie irgendeine Sprache, um Transition Systems zu beschreiben. Also irgendwie Zeitpunkt t gleich 0 ist das gültig und Zeitpunkt t gleich 1 ist das gültig. Und das sind die Übergänge. Das ist dann halt irgendwie eine spezielle Art von Source Code halt.
Und man muss das dann halt verstehen. Man muss diese Sprache kennen, um das verstehen zu können. Aber das darf man dann schon annehmen. Also wenn dann irgendwie sich eine Prüferin das anschaut, dann sagt man: Okay, wenn ich schon mal von Logik gehört habe, kann ich das irgendwie nachvollziehen und kann irgendwie sehen, dass da jemand nicht absolut Müll produziert hat. Genau. Und so am Beispiel Isabel, was so ein Beweisassistent ist, also da schreibe ich halt tatsächlich menschenlesbare Beweise.
Also ich habe eine Skriptsprache, wo ich so strukturierte Beweise, wie man es auch aus einer Mathevorlesung oder so kennt, also gegeben, sei x beliebig und fest und dieses und jenes. Und das kann ich als Mensch halt tatsächlich dann auch lesen. Und das Tool generiert mir da auch, also Isabel hat so eine Stärke in so auch so Dokumentengenerierung, wo ich diese Beweise dann eben lesen kann, um sie in einem Paper zu veröffentlichen oder sonst irgendwas.
Und es ist garantiert, dass ich diesen Output nur bekomme, wenn der Assistent in der Lage war, das komplett einmal durchzurechnen. Also ich habe das schon die Tatsache, dass ich diesen Code irgendwo hinpacken kann, ist der Beweis dafür, dass die Maschine da wirklich einmal verifiziert hat, dass es stimmt. Und das, was ich dann in der Hand habe, ist etwas, was ein Mensch auch nachvollziehen kann. Das sind natürlich Experten dann.
Also da muss man dann schon irgendwie Logik, also wie mathematischer Beweis kann auch nicht jeder vielleicht verstehen, was drinsteht. Aber man kann es nachvollziehen. Ja, ja. Wenn ich jetzt so eine Software habe, wie sieht es denn da aus, wenn ich jetzt an Änderungen rangehe? Ist es einfach, dann diesen Beweis nochmal zu machen oder weil ich schon so viel vorgearbeitet habe? Oder ist das viel Aufwand, weil ich nochmal ganz andere Dinge durchdenken muss?
Ich würde sagen, es hängt stark davon ab, auf welchem wo sich was verändert. Also in der abstrakten Beschreibung, in der Formalisierung. Also ich würde, also meine Erfahrung mit, ich habe in Isabell halt gearbeitet und genau so ein ganz basales Ding mal geändert. Und das zieht sich dann, das merkt man durch die komplette Beweisbasis durch. Also da habe ich halt irgendwie ein Jahr dran gesessen, um nochmal alle Beweise nachzuziehen und auf diese neue Sprache zu mappen.
Also das kann passieren, weil auch soweit ich weiß, halt diese Art von, das ist ja ein bisschen wie Software, aber da hat auch Modularisierung irgendwo drin. Also ich habe Teile, die sich importieren, aber die sind eben nicht. Ich habe zum Beispiel nicht so etwas wie Information Hiding oder eben lose Kopplungen, die mir in einem Software-System erlaubt, etwas auszutauschen, weil es ja keinen Sinn macht. Ich möchte ja über die Interna sprechen können.
Deshalb muss ich sie, das würde keinen Sinn ergeben für irgendeine Datenstruktur, die ich definiere und wo ich sage, später will ich etwas darüber zeigen, zu sagen, ja, aber ich verrate dir nichts über die Daten. Ich kann da ein konkretes Beispiel dafür machen. In C-Programmen hat man sehr oft das Problem, dass ja im Prinzip jeder in jeden Speicher reinschreiben kann. Also ich habe irgendwo einen Pointer und da muss ich halt irgendwas reinschreiben gegebenenfalls.
Und da ist ein ganz, ganz dickes Brett für diese Tools, das zu bohren, dass man sagen kann, okay, das ist jetzt Modul A und das hat jetzt diesen Speicherbereich und der pfuscht jetzt bitte mal nicht in den Modul B drin rum. Das ist etwas, was ich erst noch zeigen muss, was ich erst noch beweisen muss, weil wenn ich ein C-Programm anschaue, dann sehe ich das nicht, ob das der Fall ist oder nicht. Und da gibt es dann so eine Logik, die nennt sich Separation Logic.
Separation Logic heißt, weil es da einen Separated Heap gibt. Also es gibt dann verschiedene Bereiche im Heap. Und immer wenn ich dann da irgendwas ändere an der Pointerstruktur, muss ich die ganzen Separation Beweise nochmal neu machen. Weil es halt leider so ist in C. Da habe ich eben diese Speichersicherheit nicht. Das ist dann, wenn ich eine andere Programmiersprache hätte, eine funktionelle Programmiersprache zum Beispiel, habe ich das Problem gar nicht.
Da tritt das nicht auf, weil ich nicht einfach irgendwo darin poken kann in diesen Speicherteil. Und es ist halt leider so, wir sind leider in den Beweisern noch nicht so schön modular, wo man irgendwie sowas austauschen kann und dann geht es einfach trotzdem. Genau, das ist halt schwierig.
Wenn ich jetzt aber bloß irgendwo in einem Detail, in einem internen Algorithmus ändere und dadurch aber sich die Garantien des Algorithmus nicht ändern, zum Beispiel ich mache den jetzt effizienter oder keine Ahnung, ich habe noch einen zweiten Algorithmus, den ich manchmal auswähle, weil der dann irgendwie schneller ist oder sonst irgendwas.
Also solche kleinen Sachen, wenn sich das irgendwie so auf ein Modul beschränkt, dann komme ich meistens damit aus, das wirklich nur an der Stelle zu ändern. Aber sobald ich halt zum Beispiel Datenstruktur anpasse, dann habe ich praktisch verloren. Also das ist leider so. Ja, dann ändert sich halt genau der Gegenstand, wenn ich das nochmal anschaue. Aber ganz häufig gibt es halt so, gerade so in der Technologie, also in Implementierungsdetails haben die gar nicht so eine Auswirkung auf das.
Also tatsächlich Refactorings machen wir ja genau mit diesem Blick. Verhalten soll sich nicht ändern, aber dann kann ich schon ganz häufig in die Situation kommen, dass sich an der eigentlich abstrakten Beschreibung gar nichts ändert. Da muss ich vielleicht einen zusätzlichen Beweis nochmal führen, der nachweist, dass dieses Verhalten erhalten bleibt. Aber der Rest kann dann einfach so bleiben.
Dann sage ich halt okay, das gilt ja alles noch, weil ich ja nachgewiesen habe, dass sich das deckt in den relevanten Aspekten. Ja, verstehe. Superspannend. Ich muss eine Frage stellen. 2024 musst ihr auf den Tisch kommen. Wie kann euch KI helfen? Gibt es da irgendwas oder ist das kein Thema in dem Bereich? Da sind wir schon längst dran. Also ich sage jetzt mal wir als Community. Auch wieder das Tool Isabel. Ihr merkt vielleicht schon, wir haben ein Lieblingstool.
Da gibt es schon seit zehn Jahren oder vielleicht sogar noch länger, damals hat man es doch Machine Learning genannt, Unterstützung. Und zwar benutzt man da das Tool oder diese Unterstützung, um schneller Beweise schreiben zu können. Also ich habe ganz oft das Problem, dass ich in Isabel irgendwie ein paar Theoremen, ein paar Lemmas, ein paar Eigenschaften hinschreibe. Dann denke ich mir so keine Ahnung, wie ich das jetzt beweise. Klingt irgendwie intuitiv verständlich.
Dann hat Isabel auch so ein Tool, was erstmal so Tests laufen lässt, um zu gucken, ob das so plausibel ist. Dann denke ich mir so okay, irgendwie muss ich das implementieren. Und eine Unterstützung, die mir eben das erlaubt, so Beweise zu schreiben, Beweise zu generieren. Das heißt lustig, was ist Sledgehammer? Mit einem großen Hammer da drauf hauen, bis die Aussage weggeht. Und diese Sledgehammer ist eigentlich ein ganz cooles Konzept. Das sucht sich aus dem Kontext relevante Fakten raus.
Also so ähnlich, wie wenn ich jetzt mir eine Idee vorschlagen würde, möchtest du vielleicht diese Methode aufrufen, die schaut irgendwie richtig aus. Sucht der verschiedene Fakten raus, die ich schon kenne aus dem Liebung, tut die dann in irgendwelche automatischen Tools rein und schaut, ob das funktioniert.
Und das hat schon seit längerem so so eine Art Machine Learning Fähigkeiten, wo es dann zum Beispiel sagt, okay, also dieses Fakt hier, das tritt erstaunlich häufig auf und das funktioniert erstaunlich häufig. Und dann schlägt es das halt dann öfter vor. Also solche Sachen gibt es. Und ich glaube tatsächlich auch, also das ist das eine und das andere ist, ich glaube tatsächlich auch ChatGPT versteht Isabelle. Also ich habe schon von Studis gehört, die das auch mal benutzt haben.
Ich weiß allerdings nicht, wie gut es da funktioniert. Das kann ich nicht aussagen. Aber das Thema ist auf jeden Fall, also es gab schon immer eine große Überschneidung in der Web-Community beim Thema AI, also das Classic AI sozusagen vor dem ganzen LLM Zeugs, Machine Learning und sowas. Und diesen Beweisdinger. Und weil man das immer schon gesagt hat, das ist eigentlich der beste Use Case. Ich habe eine Aussage, die will ich beweisen. Die wird dann eh nochmal geprüft.
Wie der Beweis ausschaut, ist mir eigentlich völlig egal. Der wird eh nochmal überprüft. Und ja, go wild. Also versuche halt irgendwie diesen blöden Beweis zu erzeugen. Ja, ja. Genau. Also die Hauptherausforderung, gerade wenn man in so Tools wie Isabelle unterwegs ist, dass der Computer irgendwie bis zu einem bestimmten Punkt kommt und dann die Arme hochreißt und sagt: "Okay, jetzt hier muss ich mal aufhören, sonst werde ich nicht fertig mit dem Suchen der Lösung."
Und da kann genau so Machine Learning, genauso wie es Lars beschrieben hat, halt sehr weiterhelfen. Also einem sehr, sehr viel Aufwand im Beweis finden und aufschreiben ersparen. Es funktioniert verdammt gut. Also das ist schon häufiger so: "Ja, cool, fällt da die Lösung raus?" Und dann ist es: "Okay, ich bin fertig." Ja, ja, genau. Und wir haben halt immer noch den Netz in den doppelten Bündner. Ja. Also wir sind zum Beispiel, Halluzinationen sind kein Problem.
Dann würde dann einfach der Beweischenker sagen: "Keine Ahnung, was du jetzt hier willst von mir. Stimmt nicht. Dann muss ich halt nochmal versuchen." Aber also egal, was für krudes Zeug sozusagen dann aus der AI herausfällt, wird eh immer nochmal unabhängig davon überprüft. Insofern kann ich da völlig bedenkenlos wilde Sachen machen. Genau, also Isabelle glaubt seinem eigenen AI nicht. Ja, ja. Genau. Das ist ja auch wichtig. Das ist wichtig. Ja, das ist schon wichtig. Kontrollieren.
Ja. Bianca, Lars, vielen Dank für diese Einsichten. Das fand ich echt spannend, mal einen ganz anderen Blick, auch nochmal auf Qualität, auch auf Beweisführung und was da möglich ist. Danke euch sehr dafür. Ich wünsche euch noch viel Spaß auf der Konferenz. Einen tollen Vortrag heute. Dir auch. Und dann irgendwann eine gute Heimreise. Vielen Dank. Ja, danke. Danke. Danke. Danke. Untertitelung des ZDF, 2020