TU München  Informatik  Software & Systems Engineering  Theorem Proving Group  Lehre

Sommersemester 2004
Semantik von Programmiersprachen

Prof. Tobias Nipkow



 
 
 
 Inhalt  Übung  Literatur

Bereich:  Info III, Wahlpflichtvorlesung: 4 Std. (+2Ü), oder Info I, vertiefend zu Übersetzerbau (4 Std.)
Zeit und Ort: Mo, 8:30-10:00, MI 00.04.011
Fr, 8:30-10:00, MW 0350
Beginn: Mo, 19.04.2004
Zentralübung: Mi, 16:15-17:45, MI 00.04.011, erstmalig am 21.04.2004
Auf der Seite der Übung finden Sie Übungsblätter, Merkblätter und den Fragebogen aus der ersten Vorlesung.
Übungsleitung: Clemens Ballarin

Hörerkreis: Studenten/-innen der Informatik und Mathematik

Voraussetzungen: Vordiplom

Hinweis: Die Vorlesungen werden in diesem Jahr auf Deutsch gehalten.

Empfehlenswert für:
Für eine spätere theoretische Beschäftigung mit Programmiersprachen ist diese Vorlesung unabdingbar. Es bestehen ausserdem starke Querbezüge zu den Gebieten Logik, Programmverifikation und Lambda-Kalkül.

Lernziele:

Im Gegensatz zu früheren Jahren werden wir uns diesmal auf operationale Semantik konzentrieren und mit dieser Technik große Teile von Java, der JVM und eines Übersetzers behandeln. Dies ist ein Experiment!

Contents:
Starting with a simple programming language with only while-loops, we progress to a small but realistic object-oriented language, its virtual machine, and a simple compiler.

  1. Introduction

    2. The syntax of WHILE. Concrete vs abstract syntax. Evaluation of arithmetic and boolean expressions.(Isabelle [pdf][ps.gz])

  2. Operational Semantics

    1. Big-step semantics

      2. The rules. Derivation trees. Lemma while b do s is equivalent to if b do s;while b do s else skip.(Isabelle[pdf][ps.gz])
    2. Rule induction

      3. Inductively defined sets and the principle of rule induction. Examples: natural numbers and transitive reflexive closure, together with proofs of various closure properties. Rule induction for big-step semantics of WHILE. Theorem: WHILE is deterministic (Isabelle[pdf][ps.gz])
    3. Small-step semantics

      4. The rules [pdf][ps.gz]. Derivation sequences. Theorem: Agreement of big-step and small-step semantics.(Isabelle[pdf][ps.gz])
    4. Extensions of WHILE
      1. Nondeterminism. Big-step semantics hides nontermination. Small-step semantics more appropriate.
      2. Parallelism. Big-step semantics not possible. Interleaving small-step semantics.
    5. Application: a compiler for WHILE

      6. A 3-instruction machine. Its operational single-step semantics. The compiler. Detailed proof of the equivalence of running the source program and running the compiled program.(Isabelle [pdf][ps.gz])

  3. Semantics of Inductive Definitions


    4. A set theoretic treatment of rules. Definition: The set IR defined by a set of rules R is the least R-closed set.
    1. The derivation of rule induction.
    2. Theorem: IR is the least fixpoint of the consequence operator induced by R. If R is finitary, IR is the union of all finite iterations of R starting from the empty set.

  4. Jinja - A Java-like Programming Language


    5. Roughly speaking, Jinja is a subset of Java that demonstrates the key features of object-oriented programming: objects, classes, inheritance, method overriding, and dynamic method dispatch.
    1. Formal preliminaries
    2. Syntax
    3. Big step semantics
    4. Small step semantics
    5. Exceptions
    6. Equivalence of big and small step semantics
    7. Type system
    8. Well-formedness
    9. Type safety Well-typed programs do not go wrong.

  5. The Jinja Virtual Machine (JVM)


    6. The Jinja VM is a close relative of the Java VM, a high-level machine independent typed assembly language together with an abstract machine executing programs in this language.
    1. JVM
    2. Type system
    3. Bytecode Verifier
Disclaimer: The concentration on Java does not mean that we consider Java the best programming language in the world.

Übungsschein:
Einen Schein erhält, wer mindestens 40% der Punkte aus den Hausaufgaben und Programmieraufgaben erreicht und erfolgreich an der Semestralprüfung teilnimmt.

Literatur:
Die Vorlesung orientiert sich zu Beginn stark an den ersten beiden der folgenden Bücher:

Literatur zu Jinja


 

Clemens Ballarin Last modified: 16 June 2004