Formale Methoden werden als effektive, aber unangemessen komplexe Methode zur Gewährleistung der Zuverlässigkeit von Software angesehen. Die dafür verwendeten Tools unterscheiden sich erheblich von denen, die dem Programmierer bekannt sind. Dieser Artikel wurde mit dem Ziel verfasst, den Schwellenwert für die Eingabe dieses Toolkits zu senken. Ich werde das
Modellprüfsystem nicht verwenden, um schwierig formulierte Aufgaben der Softwarespezifikation zu lösen, sondern um ein Rätsel zu lösen, das selbst für Schüler verständlich ist.
Sie befinden sich in einem direkten Korridor mit sieben Zimmern auf einer Seite. In einem von ihnen ist eine Katze. In einem Schritt können Sie in einen der Räume schauen, wenn es eine Katze gibt, wird sie gefangen. Sobald sich die Tür schließt, zieht die Katze in einen der Nachbarräume zu dem Raum, in dem sie sich befand. Die Aufgabe ist es, die Katze zu fangen.
TLA + und zeitliche Logik
Es gibt viele Werkzeuge, die solche Probleme lösen können. In solchen Fällen werden häufig
SMT-Löser verwendet. In der Regel verwenden solche Systeme die übliche Prädikatenlogik, und das Ausdrücken der Abfolge von Aktionen ist ziemlich kompliziert (Sie müssen so etwas wie ein Array verwenden, mit dem Sie nicht sehr bequem arbeiten können).
TLA + verwendet eine zeitliche Logik, die es ermöglicht, den Status des Systems in einer Anweisung sowohl im aktuellen als auch im nächsten Schritt zu verwenden.
CatDistr' = CatDistr \ {n}
Diese Bedingung besagt, dass die Gruppe von Räumen, in denen sich die Katze nach Überprüfung des Raums n befinden kann, mit der Gruppe von Räumen übereinstimmt, aus denen n entnommen wurde (wenn die Katze dort war, wird sie gefangen und es gibt nichts mehr zu tun).
In imperativen Programmiersprachen entspricht dies in etwa der Zuweisung eines neuen Werts für eine Variable, berechnet aus dem alten.
Ein bisschen über Sets
Wie Sie verstehen, wird die Position der Katze durch eine Variable mit der Menge aller möglichen Räume modelliert und nicht durch einen bestimmten Raum, wie dies in einem Simulationssystem der Fall wäre. Die Verwendung des Satzes möglicher Werte anstelle eines bestimmten Werts ist eine häufig verwendete Technik bei formalen Methoden, die für unerfahrene Programmierer Schwierigkeiten bereitet. Daher habe ich eine Aufgabe gewählt, bei der die Verwendung von Mengen angemessen ist.
Programmstruktur in TLA +
Im einfachsten Fall besteht das Programm aus Deklarationen und Anweisungen (Prädikaten), die den Anfangszustand, die Beziehung zwischen dem aktuellen und dem nächsten Zustand und die Invariante beschreiben, die in allen verfügbaren Zuständen ausgeführt werden muss. Hilfsprädikate können ebenfalls vorhanden sein. Prädikate können parametriert werden.
---- MODULE cat ------------------------------------------------------------- EXTENDS Integers CONSTANTS Doors VARIABLES CatDistr, LastDoor Init == /\ CatDistr = 0..Doors /\ LastDoor = -1 OpenDoor(n) == /\ CatDistr' = 0..Doors \intersect UNION { {x-1, x+1} : x \in CatDistr \ {n} } /\ LastDoor' = n Next == \E door \in 0..Doors : OpenDoor(door) CatWalk == CatDistr /= {} =============================================================================
Die erste und letzte Zeile sind die Syntaxfunktionen der Moduldeklaration.
== bedeutet "per Definition gleich", während ein einzelnes
= genau die Gleichheit der berechneten Werte der Ausdrücke ist.
Doors ist eine Modellkonstante, die in der Konfigurationsdatei festgelegt werden muss.
CatDistr - die Verteilung der Katze in den Räumen.
Die LastDoor-Variable, der zuletzt überprüfte Raum, wird zur besseren Lesbarkeit der Programmausgabe eingegeben. Bei großen Modellen können solche Variablen das Programm erheblich verlangsamen, indem sie die Anzahl der analysierten Zustände erhöhen (da der Zustand jetzt einen Verlauf seiner Entstehung enthält und dieselben Zustände, die auf unterschiedliche Weise erstellt wurden, nun unterschiedlich sind).
Das Prädikat Init beschreibt den Anfangszustand (0..Doors ist die Menge aller Räume). OpenDoor (n) beschreibt, was passiert, wenn Sie die Tür zu Raum n öffnen (im schlimmsten Fall ist die Katze nicht da - sonst haben wir ihn erwischt).
Das nächste Prädikat sieht etwas seltsam aus - es gibt einen Raum, in den man schauen kann. Tatsache ist, dass die Existenz von etwas bedeutet, dass TLA + nicht weiß, in welchen Raum wir schauen werden, und daher in allen Fällen die Richtigkeit der Invariante überprüft.
Es wäre klarer zu schreiben
Next == OpenDoor(0) \/ OpenDoor(1) \/ ... \/ OpenDoor(Doors)
Dann funktioniert unser Code jedoch nur mit einer festen Anzahl von Räumen. Es ist besser, ihn parametrisiert zu machen.
Schließlich ist die CatWalk-Invariante viele Räume, in denen die Katze möglicherweise nicht leer ist. Die Verletzung der Invariante bedeutet, dass die Katze dort gefangen wurde, wo sie ursprünglich war. Bei der Überprüfung der Spezifikation bedeutet eine Verletzung der Invariante einen Fehler, aber wir verwenden das Tool nicht für den vorgesehenen Zweck, und der gefundene „Fehler“ bedeutet die Lösung des Problems.
Modellkonfiguration
CONSTANTS Doors = 6 INIT Init NEXT Next INVARIANT CatWalk
Hier ist alles einfach - wir haben die Anzahl der Räume, die Anfangsbedingungen, die Bedingungen für die Zustandsänderung und die zu testende Invariante angegeben.
Das Modell wird über die Befehlszeile
tlc2 -config cat.cfg cat.tla gestartet .
TLA + verfügt über eine erweiterte Benutzeroberfläche, die vom tla-toolbox-Team gestartet wurde. Leider versteht er nicht, dass .cfg-Dateien und Modellparameter über das Menü konfiguriert werden müssen.
Fazit
Bei dieser Aufgabe fiel alles ziemlich einfach aus. Praktisch bedeutende Fälle der Anwendung formaler Methoden erfordern natürlich viel umfangreichere Modelle und die Verwendung verschiedener Sprachkonstruktionen. Ich hoffe jedoch, dass das Lösen solcher Rätsel eine einfache und nicht langweilige Möglichkeit bietet, formale Methoden in Arbeitsprojekten zu implementieren.
→ Die Aufgabe wurde
hier gefunden
Nur für den Fall, ein einfaches Programm zur
interaktiven Lösungsüberprüfung . Materialien für das
Studium von TLA + . Ein weiteres Modellprüfsystem, Alloy, wird
hier beschrieben.