Theorie und Implementation objektorientierter Programmiersprachen

Zeitplan

Vorlesung 1: Einführung

Die Geschichte und wesentliche Konzepte der objekt-orientierten Programmierung werden kurz wiederholt. Sicherheitskonzepte wie Datenkapselung und Subtyping werden durch Typsysteme realisiert, die wir grob definieren und in statische und dynamische Systeme einteilen. Anhand von drei Beispielen, die Schwächen von JAVA's Typsystem aufzeigen, betonen wir die Schwierigkeit, intuitive und korrekte Typsysteme zu entwerfen. Die Spezifikation und Implementierung von Typsystemen für objekt-orientierte Programmiersprachen wird den Schwerpunkt der Vorlesung darstellen.

Material:

• Folien: overview.pdf overview.ps.gz overview.dvi
• Beispiel: Cloning cloning.java correctCloning.java
• Beispiel: Equality eq.java
• Beispiel: Arrays arrays.java
• Webseite: Geschichte der Programmiersprachen

Vorlesung 2: Ungetypte arithmetische Ausdrücke

Anhand einer rudimentären Teilsprache der Ausdrücke von JAVA führen wir folgende Begriffe ein:

• Externe Syntax
• Interne Syntax, als Grammatik oder induktiv definierte Menge
• Inferenzregeln
• Strukturelle Induktion und strukturelle Rekursion
• Operationale Semantik (small-step)
• Normalformen und Werte

Material:

• Skript: arith.ps arith.ps.gz

Vorlesung 3: Algebraische Datentypen in JAVA

Zuerst beweisen wir ausführlich, dass die in Vorlesung 2 vorgestellte Einzelschritt-Semantik deterministisch ist. Dieser Beweis dient als Modell für Beweise über induktiv definierte Relationen. Sodann stellen wir eine Methode vor, algebraische Datentypen und strukturell rekursive Funktionen in JAVA zu simulieren.

Material:

• Termbäume in JAVA: arith-1.java
• Termbäume in Haskell: arith-1.hs
• Einzelschritt-Semantik in JAVA: arith-2.java
• Einzelschritt-Semantik in Haskell: arith-2.hs

Eine kurze Diskussion verschiedener Stile für die Repräsentation algebraischer Datentypen in JAVA findet sich in dem Artikel Why Visitors? von Jens Parlsberg.

Vorlesung 4: Getypte arithmetische Ausdrücke

Zur Klärung der Beziehung zwischen small-step und big-step-Semantik beweisen wir, dass eine Folge von Einzelschritt-Auswertungen, die in einem Wert endet, auch mit einem "Big-step" auf einmal erledigt werden kann.
Dann führen wir Typen und die Typisierungsrelation für arithmetische Ausdrücke ein und definieren die Begriffe Typsystem, entscheidbares Typsystem, deterministisches Typsystem, Typprüfung (type checking), Typinferenz und Typsicherheit ein. Von den zwei Eigenschaften Fortschritt und Typerhaltung, die Typsicherheit charakterisieren, zeigen wir die zweite für unsere Sprache der arithmetischen Ausdrücke.

Material:

• Mitschrift von Cyril Bitterich: Types.pdf Types.ps.gz
• Typprüfung und Typinferenz in Haskell: Arith.hs

Vorlesung 5: Ungetypter Lambda-Kalkül I

Der Lambda-Kalkül wird eingeführt, der den Kern funktionaler Programmiersprachen darstellt und in dem sich alle Programmkonstruktionen repräsentieren lassen. Behandelt werden Variablen und Bindung, α-Gleichheit, β-Reduktion und verschiedene Auswertungsstrategien. Schliesslich wird anhand der Church'schen Booleans gezeigt, wie man im Lambda-Kalkül programmieren kann.

Material:

• Mitschrift von Cyril Bitterich: Lambda.pdf Lambda.ps.gz

Vorlesung 6: Ungetypter Lambda-Kalkül II

Wir studieren weitere Beispiele von kodierten Datentypen im Lambda-Kalkül: Paare und natürliche Zahlen. Wir definieren Nachfolger, Addition, Test auf Null und Vorgänger-Funktion durch Lambda-Terme. Schliesslich betrachten wir den Lambda-Kalkül als Objekttheorie und definieren Substitution formal als strukturell rekursive Funktion.

Material:

• Skript: lambda.ps lambda.ps.gz

Vorlesung 8: Einfach Getypter Lambda-Kalkül I

Zuerst definieren wir Typisierung und Auswertung für Booleans. Dann führen wir den einfach getypten Lambda-Kalküein. Für die Typisierungs der Variablen benötigen wir eine Typisierungskontext. Wir zeigen den ersten Teil der Typsicherheit: Fortschritt.

Material:

• Mitschrift von Cyril Bitterich: Getypter-Lambda-Kalkuel.pdf Getypter-Lambda-Kalkuel.ps.gz

Vorlesung 9: Einfach Getypter Lambda-Kalkül II

Wir zeigen Schwächungs- (Weakening), Stärkungs- (Strengthening) und Substitutionseigenschaft für Typherleitungen in einfach getypten Lambda-Kalkü und beweisen damit Typerhaltung unter Reduktion. Desweiteren führen wir Paare (Produkttyp), und den Singleton-Typ Unit ein.

Vorlesung 10: Erweiterungen des Einfach Getypten Lambda-Kalküls

Wir behandeln Sequenzen, Let, Records, und Rekursion.

Material:

• Skript: Übersicht über Syntax, Auswertung und Typisierung: extensions.ps.gz

Vorlesung 11: Referenzen

Wir führen die ersten nicht-funktionalen Konzepte ein: Referenzen und Wertzuweisung im Stil von SML. Die Auswertungssematik wird erweitert um den Zustand des Speichers, Typisierung um Speichertypen.

Vorlesung 12: Untertypen

Wir führen das Konzept von Untertypen (Subtypes) ein beweisen, dass die Subtyp-Relation entscheidbar ist.

Material:

• Skript: subtyping.ps.gz

Vorlesung 13: Objekt-orientiertes Programmieren

Wir demonstrieren, wie man in der vorgestellten funktionalen Sprache wesentliche Konzepte objekt-orientierter Programmierung simuliert: Dynamic dispatch, Kapselung, Schnittstellen und Untertypen, Vererbung und sp\"ate Bindung.

Material:

• Mitschrift Cyril: OOProgramming.pdf OOProgramming.ps.gz

Vorlesung 14: Featherweight Java

Wir stellen Featherweight Java vor, eine minimale objektorientierte Teilsprache von Java, die Vererbung und Subtyping modelliert. Dazu Typ- und Auswertungsregeln und Aussagen zur Typsicherheit.

Material:

• Folien Featherweight Java von Robert Harper.
• Paper Featherweight Java: A minimal core calculus for Java and GJ von Atsushi Igarishi, Benjamin Pierce und Philip Wadler.

Übung 1: Wiederholung einiger Grundkonzepte von JAVA

Wir wiederholen einige Konzepte der objektorientierten Programmiersprache JAVA:

• Statische Methoden und main
• Kontrollstrukturen: for, if, try
• Ausnahmebehandlung
• Klassen und Instanzen
• Shallow und Deep Cloning

Material:

• Webseite: JAVA-Kurs von Dr. Thorsten Altenkirch
• Beispiel: MyHelloWorld.java
• Beispiel: printArgs.java
• Beispiel: squares.java
• Beispiel: Person.java

Übung 2: Besprechung Übungsblatt 1

Besonders eingegangen wird auf direkte Beweise durch Induktion, die ohne Widerspruch auskommen und daher konstruktiv sind. Ausserdem wird die deterministische Einzelschritt-Auswertungssemantik detailliert besprochen.

Übung 3: Parsen

• Ströme
• Lexer (auch Scanner genannt)
• Parser

Material:

• Ströme in SML: stream.sml
• Ströme in GJ: streams.java (kann leicht in gültigen JAVA-Code umgewandelt werden)
• Haskell-Implementation eines Parsers für Differenzenausdrücke: Arith_2.hs Lexer_1.hs Parser_1.hs Test_1.hs

Übung 4: Besprechung Übungsblatt 3

Diskutiert wird subject expansion, d.h. ob Typerhaltung auch unter Expansion (im Gegensatz zu Reduktion) eines Terms gilt. Der Unterschied zwischen abgeleiteten Regeln (derived rules) und zulässigen Regeln (derived rules) wird besprochen.

Übung 5: ausgefallen

Übung 6: Namenlose Repräsentation von Lambda-Termen nach Nicolas de Brujin

Vorgestellt wird eine Repräsentation von Lambda-Termen, die das Problem der α-Äquivalenz und der Variablenumbennenung bei Substitution beseitigt. Zuerst beschrieben wurde diese Methode von Nicolas de Bruijn (1972) für sein Projekt AutoMATH.

Material:

• Mitschrift von Cyril Bitterich: deBruijn.pdf

Übung 7: Small-step Semantik für den Lambda-Kalkül

Wir definieren call-by-name, call-by-value, normaler und applikativer Auswertung für den Lambda-Kalkül formal.

Übung 8: Besprechung Blatt 6

Ausserdem diskutieren wir subject expansion für den getypten Lambda-Kalkül und zeigen Beispiele für Funktionen höherer Ordung.

Übung 9: Einführung und Beseitigung

Wir untersuchen die Einteilung von Termen in Konstruktoren und Selektoren (Anwendungen). Daraus ergibt sich eine Klassifikation der Typregeln in Einführungs- (Introduction Rules) und Beseitigungs-Regeln (Elimination Rules). Berechnung ist die Entfernung von Konstruktor-Selektor-Paaren.

Übung 10: Typerhaltung und Fortschritt für fix (Rekursion)

Wir wiederholen die Definition rekursiver Funktionen durch Fixpunkte und beweisen Typerhaltung und Fortschritt. Ausserdem besprechen wir Typinferenz für den Lambda-Kalkül mit Booleans.

Material:

• Typinferenz und Typprüfung in Haskell: DeBruijn.hs Test.hs
• Typinferenz in JAVA: infer.java

Übung 11: Besprechung Blatt 8

Wir besprechen die Aufgaben mit Referenzen von Blatt 8. Dabei geht es auch um Simulation von "OOP" im Lambda-Kalkül mit Referenzen und Records.

Material:

• Teillösung der Aufgaben als SML-Code: ass8.sml

Übung 12: Besprechung Blatt 9

Wir diskutieren ausserdem die Subtyping-Regel für Funktionstypen in JAVA und kommen zu dem Schluss, dass sie dort nicht vorhanden ist, da es sonst Probleme mit overloading geben würde.

Material:

• Funktions-Untertypen in JAVA: testSubtypeArrow.java (kompiliert nicht!!)
• Lösung der Aufgabe 2: Pierce, Aufgabe 15.2.3 (2) und (3) [ersetze "Top" durch "Bool"]
• Lösung der Aufgaben 3 und 4 in Haskell: Subtyping.hs mit Test.hs, benutzt balancierte Bäume RedBlack.hs

Übung 13: Besprechung Blatt 10

Wir verbessern Blatt 10: Objekt-orientierte Programmierung im getypten Lambda-Kalkuel mit Records, Rekursion und Subtyping.

Material:

• Musterlösung: sol10.txt, und als ausführbares SML-Programm: sol10.sml

AndreasAbel Last modified: Tue Jul 16 14:15:17 CEST 2002