Formale Entwicklung objektorientierter Software

Praktikum im Wintersemester 2007/2008

Das regelmäßige wöchentliche Treffen findet Mittwochs von 17.30 bis 19.00 Uhr im Raum 301 statt.

1. Termin am 24.10.07: Vorbesprechung
   • Folien (pdf)
   • 1. Übungsblatt (pdf)
2. Termin am 31.10.07: Sequenzenkalkül, Compiler-Verifikation
   • Folien (pdf)
   • 2. Übungsblatt (pdf, aufgabe1.tar.gz, aufgabe2.tar.gz, aufgabe3.tar.gz, CompilerKorrektheit.pdf)
3. Termin am 07.11.07: Induktion, Compiler-Verifikation
   • Folien (pdf)
   • 3. Übungsblatt (pdf, aufgabe1.tar.gz, aufgabe2.tar.gz, aufgabe3.tar.gz, aufgabe4.tar.gz)
4. Termin am 14.11.07: JML
   • Folien (pdf)
   • 4. Übungsblatt (pdf, core.tgz, Blatt4.java)
5. Termin am 21.11.07: ESC/Java2
   • Folien (pdf)
   • 5. Übungsblatt (pdf, Bag.java, Amount.java, C1.java, C2.java, C3.java, C4.java)
6. Termin am 28.11.07: Übung
7. Termin am 05.12.07: Dynamische Logik
   • Folien (pdf)
   • 6. Übungsblatt (pdf, aufg2.tgz, aufg3.tgz)
8. Termin am 12.12.07: Dynamische Logik II
   • Folien (Teil 1, Teil 2)
   • 7. Übungsblatt (pdf)
9. Termin am 20.12.07 (Donnerstag, SR 131): Übung, Start des Praktikumsprojekts
   • 8. Übungsblatt (pdf, core.tgz)
   • 9. Übungsblatt (pdf)
10. Termin am 06.02.08
    • 10. Übungsblatt (pdf)

Materialien

• KeY
  • Die KeY-Homepage
  • Die KeY-Praktikumsversion (aktualisiert am 10.12.07): Download (Readme, externe Bibliotheken) oder Webstart
  • Die KeY-Quicktour und das darin vorgestellte Beispiel
  • Eine Kurzeinführung zum Thema prädikatenlogische Beweise in KeY
  • Das KeY-Buch (Online-Version ist uni-intern verfügbar)
• JML
  • Die JML-Homepage
  • Das JML Reference Manual
  • Eine JML-Einführung
• ESC/Java2
  • Die ESC/Java2-Homepage
  • Das ESC/Java User's Manual
• Java
  • Die Java API Specification
  • Der Wikipedia-Eintrag zu Javadoc
  • Verschiedene Java-Tutorials von Sun
• UML
  • Die offizielle UML-Spezifikation: Superstructure, Infrastructure
  • Eine kurze UML-Einführung von Borland