Formale Entwicklung objektorientierter Software

Praktikum im Wintersemester 2006/2007

Das regelmässige wöchentliche Treffen findet Mittwochs von 17.30 bis 19.00 Uhr im Raum 301 statt (erstmals am 08.11.06).

1. Vorbesprechung am 25.10.06:
   • Folien der Vorbesprechung
   • Gruppeneinteilung
   • 1. Übungsblatt (pdf)
2. Termin am 08.11.06: Einführung in JML
   • Folien (pdf)
   • 2. Übungsblatt (pdf, Blatt2.java)
3. Termin am 15.11.06: Dynamische Logik
   • Folien (pdf)
   • 3. Übungsblatt (pdf, aufg7.tgz, aufg9.tgz)
4. Termin am 22.11.06: Dynamische Logik für Java Card
   • Folien (pdf)
5. Termin am 29.11.06: Übung
   • Musterlösung 4. Aufgabe (java)
   • 4. Übungsblatt (pdf), Lösung (pdf)
6. Termin am 06.12.06: Uppaal Einführung
   • Folien (pdf)
   • 5. Übungsblatt (pdf)
7. Termin am 20.12.06: Schleifeninvarianten
   • Folien (pdf)
   • Beispiel
8. Termin am 17.01.07: Vorstellung des Model Checking Projekts
   • 6. Übungsblatt (pdf)
9. Termin am 24.01.07: Methodenkontrakte, modularisierte Programmverifikation
   • 7. Übungsblatt (pdf, BerlinBank.tgz)

Weitere Materialien

• KeY-Praktikumsversion (aktualisiert am 05.02.2007):
  • Sourcecode-Version
  • notwendige Bibliotheken und Werkzeuge (Simplify)
  • KeY-Regelreferenz
• Die KeY-Quicktour und das darin vorgestellte Beispiel
• Einige weitere Erklärungen zur Benutzung von KeY
• UML Reference Manual
• Offizielle UML-Spezifikation: Superstructure , Infrastructure
• Kurze UML-Einführung von Borland/Together
• OCL 1.3 (Spezifikation)
• Der Wikipedia Eintrag zu Javadoc
• JML
  • JML Home Page
  • JML Reference Manual
  • Eine JML-Einführung
• Uppaal Model Checker
  • Download
  • Tutorial über Uppaal und Timed Automata