Wenn Fehler in einem Programm auftreten, dann passiert bei der Fehlersuche oft dies: Man sucht und sucht und schließlich findet man den Fehler. Und erstmal gefunden, ist ganz klar und offensichtlich, was verkehrt war. Man wundert sich, wie der Fehler überhaupt hat passieren können!

Wäre es da nicht hilfreich, ein Werkzeug zu haben, mit dem man simple Denkfehler leicht erkennen kann - und zwar möglichst beim Entwurf von Software oder sogar zur Überprüfung von Ideen und Konzepten schon vorher.

Solche Werkzeuge gibt es und eines davon können Sie im Master-Kurs Interaktives Spezifizieren und Verifizieren von Softwareartefakten im Sommersemester 2023 kennenlernen und erproben: Alloy. Mehr zum Kurs in Moodle.

ChatGOPT sagt über Alloy: „Alloy ist eine formale Spezifikationssprache, die für die Modellierung und Analyse von Softwaresystemen verwendet wird. Die Sprache ermöglicht es, komplexe Systeme in einer mathematisch präzisen Art und Weise zu beschreiben und zu analysieren, um potenzielle Fehler oder Probleme zu identifizieren, bevor die Software tatsächlich implementiert wird.“ Und ausnahmsweise ist diese Aussage von ChatGPT sogar ziemlich korrekt. Ergänzend könnte man höchstens sagen, dass man mit Alloy auch bereits implementierte Software analysieren kann.

Burkhardt Renz