Diese Vorlesung wird im Wintersemester 2009/2010 zum ersten Mal in dieser Form gehalten.
Sie behandelt zwei verschiedene Spezifikationsmethoden:
- EventB
Benutzt die Methode der sukzessiven Verfeinerung. Operiert auf der abstrakten Ebene rein mengentheoretischer Notation. Das zugehörige Beweiswerkzeug heiß Rodin. - Java Modeling Language JML
Die Spezifikationen werden direkt als Annotationen in der Form spezieller Kommentare in den Java Code geschrieben. Syntax und Semantik von JML orientieren sich sehr stark an Java. Als Analysewerkzeuge werden benutzt: Ein runtime checker rac, ein Testgenerator JMLUnit, eine (unvollständige) statische Analyse ESCJava2 und ein Theorembeweiser KeY.
Die Vorlesung ist in enger Anlehnung an des Praktikum Formale Entwicklung objektorientierter Software konzipiert. Zum einen werden die zur Durchführung der Praktikumsversuche erforderlichen einführenden Erklärungen bereitgestellt, zum anderen wird der theoretische Hintergund und verwandte Themen behandelt.
