Bereich:  Wahlvorlesung für Informatics (Bachelor), Informatics (Master) und Applied Informatics (Master): 4 Std. (+2Ü), 8 ECTS Punkte.  Ausserdem Wahlpflichtvorlesung im Hauptdiplom (Theoretische Informatik).
DHP: Der Übungsschein kann als Praktikumsschein im Bereich Theoretische Informatik in die DHP eingebracht werden.  (Prüfungsordnung)
Zeit und Ort: Montags, 8:25-10:00, MW 0250 und mittwochs, 12:10-13:45, MI 00.09.022.
Beginn: Montag, 16. April
Zentralübung: Dienstags 16:15 - 17:45.  Am 17.4. und 24.4. in MI 01.11.018 (Konrad Zuse), ab dem 8.5. in MI 01.09.014 (Alonzo Church).
Übungsleitung: Clemens Ballarin
Hörerkreis: Studenten/-innen der Informatik und Mathematik
Hinweis: Die Vorlesung wird auf Englisch 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:

  • Das Verstehen der grundlegenden mathematischen Technik der operationalen Semantik um eine Programmiersprache präzise zu definieren.
  • Das Anwenden dieser Techniken auf Probleme wie Äquivalenz verschiedener Sprachbeschreibungen, Korrektheit von Übersetzern, Sicherheit von Typsystemen, Korrektheit von Programmanalysen etc.
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.
      3. Procedures. Static and dynamic scope for variables and procedures. Big-step semantics for a) dynamic scope for variables and procedures, b) dynamic scope for variables and static scope for procedures, c) static scope of variable and procedures. (See Nielson & Nielson)
    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
    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
    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. Slides

  5. Hoare Logic

    1. From Floyd to Hoare. Partial and total correctness. The rules of Hoare logic.
    2. Syntax of assertions: first-order arithmetic.
    3. Semantics of assertions and Hoare triples: validity w.r.t. a state and an interpretation of the logical variables.
    4. Soundness of Hoare logic: proof by rule induction.
    5. Completeness of Hoare logic: impossible for effective proof systems. Relative completeness: use semantics (|=) rather than proof system (|-) of the assertion language. Prove relative completeness via weakest liberal precondition and expressiveness, i.e. the ability to express the wlp in the assertion language.
    6. Verification conditions. Extraction of (weakest) preconditions and verification conditions in the presence of loop invariants. Proof of soundness and completeness of this approach.
    7. Total correctness.
    8. Extensions of WHILE
      1. Nondeterminism
      2. Arrays
      3. Procedures: The problem. An adaption rule. A complete system based on a generalized consequence rule. Completeness proof. Literature reference

  6. CoreC++ - Multiple Inheritance in C++

Disclaimer: The focus on Java does not mean that we consider Java the best programming language in the world.

Übungsschein:
Einen Schein erhält, wer erfolgreich an der Semestralprüfung teilnimmt.  Bearbeitete Hausaufgaben können auf freiwilliger Basis abgegeben werden und werden von der Übungsleitung korrigiert.

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

Literatur zu Jinja