| Typ: | Praktikum |
|---|---|
| Ort: | Raum 211, Geb. 50.34 |
| Zeit (regulär) : | Di, 17.30 - 19.00 |
| Beginn: | 26.10.2010 |
| Dozierende: |
Prof. P. H. Schmitt Prof. B. Beckert Daniel Bruns David Faragó Christoph Gladisch Christoph Scheben |
| LVNr.: | 24308 |
Motivation
Ist fehlerfreie Software möglich?
Wenn Sie die Antwort auf diese Frage interessiert und Sie schon immer einmal Software in einer Gruppe entwickeln wollten, dann ist dieses Praktikum genau das, wonach Sie suchen.
Anhand eines selbst realisierten Software-Projektes lernen Sie in einer Gruppe Aspekte der formalen Softwareentwicklung kennen und anzuwenden, d.h. Analyse, Modellierung, Spezifikation, Implementierung und Verifikation (aber z. B. auch Dokumentation). Für die Implementierung verwenden wir Java, zum Spezifizieren die Java Modeling Language (JML). Als Verifikationswerkzeuge werden z. B. ESC/Java2, JMLUnit, der JML Runtime Assertion Checker (RAC) und KeY eingesetzt.
Der in der Vorlesung "Formale Systeme" behandelte Stoff sowie Programmierkenntnisse werden vorausgesetzt. Kenntnisse aus der Vorlesung "Softwaretechnik" sind von Vorteil. In der parallel laufenden Vorlesung "Spezifikation und Verifikation von Software" werden die notwendigen theoretischen Grundlagen zum Praktikum vermittelt. Zu den einzelnen Praktikumseinheiten gibt es korrigierte und besprochene Übungsaufgaben.
Vorbesprechung am Mittwoch, dem 26. Oktober 2010, um 13:00 im Raum 211 (Geb. 50.34)
Inhalt:
Praktischer Umgang mit Spezifikationsprachen und Verifikationswerkzeugen für objektorientierte Software, wie beispielsweise
- Spezifikationssprachen: JML und JavaDL
- Verifkationswerkzeuge: rac, ESC/Java2 und KeY
Lernziele:
Die Fähigkeit Werkzeuge zur Spezifikation und Verifikation von objektorientierter Software pratkisch einzusetzen.
Organisatorisches
- Im Abstand von etwa ein bis zwei Wochen werden von den Teilnehmern Lösungen zu den Übungsblättern präsentiert. Die Teilnehmer wechseln sich mit den Präsentationen ab, aber alle Teilnehmer einer Gruppe müssen Fragen während der Präsentation beantworten können.
- Die schriftliche Abgabe zu einem Übungsblatt findet ein oder wenige Tage vorher statt und wird auf dem Blatt bekannt gegeben.
- Abwechselnd zu den Präsentationen der Teilnehmer finden Treffen zum gemeinsamen Arbeiten und für zwei Vorlesungstermine statt.
Termine
- Da der 1.11.2011 ein Feiertag ist, findet der nächste Termin am Donnerstag dem 03.11. um 14:00 statt.
Aufgaben
- Übungsblatt 1: JML, Daniel Bruns
- Übungsblatt 2: RAC und JMLUnit, David Farago
- Übungsblatt 3: ESC/Java2, Christoph Gladisch
- Übungsblatt 4: KeY , Christoph Scheben
- Übungsblatt 5: Praktikumsprojekt, Christoph Gladisch
- Übungsblatt 6: KeY , Christoph Gladisch, Christoph Scheben
Weitere Informationen und relevante Dokumente
JML
- Die JML-Homepage
- Eine JML-Einführung
- Das JML-Referenzhandbuch
- JML 5.5 herunterladen
- Online JML-Syntax-Checker