General Flashcards
1
Q
Vorteile LTL + Model Checking:
A
Entscheidbar
Gegenbeispiel wird geliefert wenn die Uberpr ¨ ufung fehlschl ¨ ¨agt
Vollautomatisches Verfahren
LTL hat einen kompakteren Vokabulars als JML
LTL ist unabh¨angig von der Programmiersprache
Bereits in der Modellierungshase anwendbar
Besser fur temporale Eigenschaften
2
Q
Vorteile JML + KeY:
A
Modularit¨at
H¨ohere Ausdrucksm¨achtigkeit
Kein Modell der Software n¨otig
Java-¨ahnliche Syntax von JML, JML ist einfacher fur Programmierer zu lesen, schreiben oder verstehen
Einfacher zu identifizieren, welcher Software-Teil die Spezifikation verletzt
besser parallelisierbar
