- 26.07.2017:
Die Nachklausur ist geplant für Mittwoch, den 11. Oktober 2017,
14–16 Uhr, im SR055. Die Anmeldungen erfolgen im
KVV.
Da alle Teilnehmenden die Klausur bestanden haben, handelt es sich um
einen Freiversuch. Daher möchte ich Sie bitten, sich bis zum 1. Oktober
2017 anzumelden. Falls sich zum 1. Oktober niemand angemeldet hat, gehe
ich davon aus, dass niemand den Freiversuch wahrnehmen möchte, und werde
die Nachklausur absagen.
- 24.07.2017:
Die Klausur ist korrigiert. Sie können Ihre Punktzahl im
KVV nachlesen. Das
Notenschema ist hier. Die Klausureinsicht
findet statt am Mittwoch, den 26.07.2017, um 16:00 Uhr
im Raum 112.
- 20.07.2017: Am Montag, den 24.07.2017 findet von 10–12
Uhr im SR 046 die Klausur
statt. Außer Schreibutensilien ist lediglich ein beidseitig handbeschriebenes DIN-A4 Blatt
als Hilfsmittel erlaubt. Bitte bringen Sie ein Personaldokument
mit Lichtbild sowie Ihren Studierendenausweis mit.
Bitte bis 10:10 Uhr die Plätze einnehmen. Klausurbeginn um 10:15 Uhr.
- 05.07.2017: Das dreizehnte Aufgabenblatt ist verfügbar.
Dies ist das letzte Aufgabenblatt.
- 29.06.2017: Das zwölfte Aufgabenblatt ist verfügbar.
Dies ist das vorletzte Aufgabenblatt.
- 22.06.2017: Das elfte Aufgabenblatt ist verfügbar.
- 15.06.2017: Das zehnte Aufgabenblatt ist verfügbar.
- 08.06.2017: Das neunte Aufgabenblatt ist verfügbar.
- 01.06.2017: Das achte Aufgabenblatt ist verfügbar.
- 25.05.2017: Das siebte Aufgabenblatt ist verfügbar.
- 18.05.2017: Das sechste Aufgabenblatt ist verfügbar.
- 16.05.2017: Der Klausurtermin wurde verlegt auf Montag,
den 24. Juli 2017, 10–12 Uhr im SR 046.
- 11.05.2017: Das fünfte Aufgabenblatt ist verfügbar.
- 08.05.2017: Die Abgabemodalitäten der Aufgabenblätter wurden geändert.
Die Aufgeben werden nun immer Donnerstags ausgegeben und sind am Dienstag 12 Tage später
in der Vorlesung abzugeben.
- 08.05.2017: Die Abschlussprüfung wird in Form einer Klausur durchgeführt. Diese
findet statt am Donnerstag, den 20. Juli 2017, von 14–16 Uhr im SR 055.
Zum Bestehen sind mindestens 50% der Punkte nötig.
- 03.05.2017: Das vierte Aufgabenblatt ist verfügbar.
- 26.04.2017: Das dritte Aufgabenblatt ist verfügbar.
- 20.04.2017: Das zweite Aufgabenblatt ist verfügbar.
- 18.04.2017: Die nächste Vorlesung findet statt
am Donnerstag, den 20.04.2017, von 14–16 Uhr, an Stelle
der Übung. In der nächsten Woche sind die Termine
für Übung und Vorlesung vertauscht.
- 01.04.2017: Das erste Aufgabenblatt ist verfügbar.
- 02.02.2017: Die Website ist online. Die erste Vorlesung findet
statt am Dienstag, den 18.04.2017 um 08 Uhr ct.
Die Übungszettel werden ausschließlich online erscheinen
und zwar hier auf dieser Seite.
- Ansätze zur Beschreibung von Semantik
- Operationell, Denotationell, Axiomatisch
- operationelle Semantik
- natürliche und strukturelle Semantik
- Nichtdeterminismus und Parallelität
- beweisbar korrekte Implementierung
- denotationelle Semantik
- Theorie der semantischen Bereiche, Fixpunkt-Theorie
- Fortsetzungssemantik
- Programmanalyse
- Axiomatische Semantik
- Programmverifikation und Laufzeitanalyse
- Semantik funktionaler Programmiersprachen, Typtheorie, Curry-Howard Isomorphismus
- Dienstag, den 18.04.2017
- Administrativa
- Einleitung
- Ziele beim Entwurf von Programmiersprachen
- Aspekte: Syntax, Semantik und Idiomatik
- Semantik von imperativen Programmiersprachen
- zentrales Konzept: der Zustand
- Ein imperatives Programm ist eine
Folge von Anweisungen. Die
Anweisungen verändern den Zustand.
Die Semantik eines imperativen Programmes
ist die Zustandsänderung, welche es
hervorruft.
- formal: Zustand: Funktion von den
Variablen zu ihren aktuellen Werten.
- Semantik: Eine Funktion, die
jedem Programm eine Funktion von der
Menge aller Zustände in die Menge
aller Zustände zuordnet.
- Donnerstag, den 20.04.2017
- Ansätze zur Definition der semantischen
Funktionen.
- operationell: definiere semantische Funktion
Schritt für Schritt, als ein
Transsitionssystem. Zwei Varianten:
definiere Transitionssystem durch Angabe
der einzelnen Schritte (small step semantics,
strukturelle operationelle Semantik) oder
globaler durch Angabe von Schlussregeln
(big step semantics, natürliche
operationelle Semantik)
- denotationell: definiere semantische
Funktion direkt durch Rückführung
auf eine mathematische Funktion.
Wichtig: Zusammengesetztheit–die
Definition darf sich nur induktiv auf die
syntaktischen Bestandteile des
Programmes beziehen.
- axiomatsich: verzichte auf vollständige
Spezifikation der semantischen Funktion.
Arbeite mit Zusicherungen, welche
bestimmte Eigenschaften des aktuellen
Zustandes widerspiegeln. Definiere ein
logisches System, welches die Beziehungen
zwischen den Zusicherungen darstellt.
- Die Beispielsprache while
- Syntax
- syntaktische Kategorien
- semantische Funktionen
- Donnerstag, den 27.04.2017 (vertreten durch Max Willert)
- Semantische Funktion für arithetische Ausdrücke
- Freie Variablen und Substitution
- Schlussregeln zur Definition einer operationellen Semantik
- Dienstag, den 02.05.2017
- Natürliche operationelle Semantik von while
- Dienstag, den 09.05.2017
- Strukturelle operationelle Semantik von while
- Dienstag, den 16.05.2017
- Eigenschaften der strukturellen operationellen Semantik
- Äquivalenz der natürlichen und der
strukturellen operationellen Semantik
- Dienstag, den 23.05.2017
- Programmabbruch in der strukturellen operationellen Semantik
- Blöcke und lokale Variablen
- Donnerstag, den 01.06.2017
- Unterprogramme mit dynamischem Gültigkeitsbereich
- Denotationelle Semantik
- Dienstag, den 06.06.2017
- Denotationelle Semantik von while Schleifen
- Fixpunktiteration
- Dienstag, den 13.06.2017
- Ordnungsrelationen
- Minima, obere Schranken, Suprema
- Kettenvollständigkeit
- Dienstag, den 20.06.2017
- Kettenvollständigkeit der
Zustandsüberführungsfunktionen
- stetige Funktionen
- Donnerstag, den 29.06.2017
- Konvergenz der Fixpunktiteration für
stetige Funktionen
- Stetigkeit der semantischen Funktionen
- Dienstag, den 04.07.2017
- Äquivalenz der denotationellen und
operationellen Semantik von while.
- Dienstag, den 11.07.2017
- Vorzeichenanalyse mit denotationeller Semantik
- Dienstag, den 18.07.2017
- Vorzeichenanalyse mit denotationeller Semantik (Fortsetzung)
- Abschluss und Ausblick
- Montag, den 24.07.2017 (10–12 Uhr, SR 046)
- Mittwoch, den 26.07.2017 (geplant, 16 Uhr, Raum 112)
Literatur
- Hanne Riis Nielson, Flemming Nielson. Semantics with Applications. An
Appetizer. Springer-Verlag, 2007
[link zu einer Vorgängerversion]
- Elfriede Fehr. Semantik von Programmiersprachen. Springer-Verlag, 1989
[link]
- Glynn Winskel. The Formal Semantics of Programming Languages. Foundations of Computing Series, MIT Press, 1993
[Skript dazu]
Empfohlene Vorkenntnisse
- Kenntnis grundlegender diskreter Mathematik, Logik und
Sprachentheorie
- Vier erfolgreiche Semester im BSc-Studiengang.
Für den Scheinerhalt muss man
-
regelmäßig an dem Tutorium teilnehmen (bei mindestens 80% der
Termine);
-
mindestens 60% der Punkte auf den Übungszetteln erreichen und
mindestens zweimal im Tutorium vorrechnen; und
- mindestens 50% der Punkte in der Abschlussklausur erreichen.
Die erfolgreiche Teilnahme am Übungsbetrieb und das Bestehen der
Abschlussprüfung sind unabhängige Leistungen.
Die Scheine sind benotet. Die Note beruht nur auf dem Ergebnis
der Abschlussprüfung.
Die Abschlussprüfung wird in Form einer Klausur durchgeführt, und
zwar am Montag, den 24. Juli 2017, von 10–12 Uhr im SR 046.
Zum Bestehen sind mindestens 50 Prozent der Punkte der Abschlussklausur nötig.
Die Vorlesung findet Dienstags von 08–10 Uhr im SR 053 statt,
die Übung
Donnerstags von 14–16 Uhr im SR 055.
Die Tutorien werden betreut von Max Willert.
Sprechzeit des Dozenten: Dienstag 14–15 Uhr in Zimmer 112 und
nach Vereinbarung.
Die Übungszettel werden jede Woche hier verlinkt. Sie werden
ausschließlich online erscheinen.
Die normale Bearbeitungszeit ist von Donnerstag zum Dienstag 12 Tage später. Die Abgabe erfolgt in
der Vorlesung.
Die Bearbeitung erfolgt in Zweiergruppen.
Übungszettel, die nach dem angegebenen Termin
abgegeben werden, zählen als nicht bearbeitet.
Nr. | Ausgabe | Abgabe |
pdf | tex | Bemerkungen |
1 |
01.04.2017 |
27.04.2017 |
|
|
|
2 |
20.04.2017 |
02.05.2017 |
|
|
|
3 |
26.04.2017 |
08.05.2017 |
|
|
[while.hs] |
4 |
03.05.2017 |
15.05.2017 |
|
|
|
5 |
11.05.2017 |
23.05.2017 |
|
|
|
6 |
18.05.2017 |
30.05.2017 |
|
|
|
7 |
25.05.2017 |
06.06.2017 |
|
|
[while2.hs] |
8 |
01.06.2017 |
13.06.2017 |
|
|
Punkteverteilung geändert |
9 |
08.06.2017 |
20.06.2017 |
|
|
|
10 |
15.06.2017 |
27.06.2017 |
|
|
|
11 |
22.06.2017 |
04.07.2017 |
|
|
|
12 |
29.06.2017 |
11.07.2017 |
|
|
vorletztes Aufgabenblatt. Punkteverteilung wurde geändert. |
13 |
06.07.2017 |
18.07.2017 |
|
|
letztes Aufgabenblatt |