8 Model-Checker
Team: Aneta Kümper, Frank Naumann, Eike Schulz
Es soll die Möglichkeit gegeben werden, die Korrektheit des
eingegebenen Programmes zu überprüfen. Dies soll in einfacher Weise dadurch
geschehen, daß überprüft wird, ob auf allen Ausführungen des Programmes die
Assertions nicht verletzt sind.
Im wesentlichen wird eine Graphsuche implementiert werde: die
abstrakte Syntax wird in einem ersten Schritt in einen (expliziten oder
impliziten) Graphen übersetzt, der danach mittels Tiefensuche nach
verletzung der Zusicherungen abgesucht wird.
Schnittstelle
Im wesentlichen mit der Gui (Abschnitt 2):
Methode start_modcheck mit Parameter eines Programmes in
abstrakter Syntax. Rückgabe: noch zu klären: entweder mittels
Ausnahme oder boolescher Wert. Auf jeden Fall wird der Gui der Zustand,
zurückgegeben wo die Verletztung auftritt. Wie die Gui darauf reagiert,
ist nicht Sache des Modelcheckerpaketes. (z.B. könnte der Zustand
gehighlighted werden.)
©Public License