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)
    • Klausur
  • Mittwoch, den 26.07.2017 (geplant, 16 Uhr, Raum 112)
    • Klausureinsicht

Literatur

Empfohlene Vorkenntnisse

Für den Scheinerhalt muss man

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.AusgabeAbgabe pdftexBemerkungen
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
Impressum