8 Model-Checker (optional)
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. Es ist freigestellt, diese
Funktionalität durch eine Übersetzung in ein bestehendes Tool zu
implementieren. Alternativ kann man es in Java implementieren (es wird
vermutlich sehr viel weniger effizient).
©Public License