Semantik von Programmiersprachen

Prof. Tobias Nipkow, Ph.D.

Bereich: III, Vorlesung: 4 Std.
Semantik kann alternativ auch als Vertiefung zu Übersetzung von Programmiersprachen in die Diplomprüfung im Bereich Praktische Informatik eingebracht werden.

Zeit & Ort: Montag 10:15-11:45 in N1070 und Freitag 9:25-10:55 in 0606.

Beginn: 2.11.1998

Übung: (Achtung: Zeit und Ort geändert!) Di 12:30-14:00 (2stündig) in 1546; Beginn: 10.11.1996
Übungsleitung: Dr. Olaf Müller
Übungsschein: Einen Schein erhält, wer mindestens 40% der Punkte aus den Hausaufgaben und Programmieraufgaben erreicht und erfolgreich an der Semestralprüfung teilnimmt.

Prüng: Wer obige Voraussetzung (40%!) erfüllt hat, kann durch eine mündliche Prüfung einen Schein erwerben. Die Prüfungen finden am 26.2. ab 9:00 statt. Bitte melden Sie Sich bis spätestens am 19.2. bei Dr. Olaf Müller an.

Die Aufgabenblätter für die Zentralübung werden regelmäßig in der Vorlesung verteilt. Für alle Aufgaben werden Lösungsvorschläge bereitgestellt. Bei Bedarf werden in der Vorlesung auch Merkblätter ausgeteilt.

Lernziele:

Beispielhafte Anwendungen der Techniken der Vorlesung auf die Programmierpsrache Java finden sie hier.

Inhalt:

  1. Operational semantics of IMP
    Syntax and operational semantics of arithemetic expressions, boolean expressions and commands. Evaluation of expressions is deterministic (by structural induction). Proof by structural induction that execution of commands is deterministic fails.
  2. Inductive definitions and rule induction
    1. Motivating examples
      Inductive definition of natural numbers. Proof that natural numbers are closed under addition. Inductive definition of the reflexive transitive closure of a binary relation. Proof that it is transitive. Indtroduction to ProofEasy, a tool for proving by clicking. Proof of examples in ProofEasy.
    2. Formal foundations
      Definition of IR as the least R-closed set or as the intersection of all R-closed sets. Proof of the principle of rule induction. Special rule induction for mixed rules. Application to execution of commands. Proof that execution of commands is deterministic.
    3. IR as a least fixpoint
      The function R-hat. Characterization of IR as an infinite union of approximations using R-hat (for finitary R).
  3. Denotational semantics
    1. Denotational semantics of IMP
      Denotational semantics of arithmetic and boolean expressions. Denotational semantics of while-loops as least fixpoints using the theory of inductively defined sets. Proof that operational and denotational semantics of expressions and commands agree.
    2. Continuous functions on complete partial orders
      Definition of cpos and continuity. Proof of the fixpoint theorem.
    3. Monotone functions on complete lattices
      Definition of complete lattice. Proof of the Knaster-Tarski fixpoint theorem.
    4. Application: An extension of IMP with random numbers
      Relational semantics easy. Problem: no distinction between possible and guaranteed nontermination. Solution: a separate denotational semantics for the set of terminating states. While-loop gives rise to a monotone but non-continuous function. Needs Knaster-Tarski to guarantee least solution. Continuity only for bounded nondeterminism.
  4. Axiomatic semantics of IMP
    1. From Floyd to Hoare. Rules of Hoare logic. Examples. Syntax, semantics and validity of assertions and Hoare triples.
    2. Thm The rules of Hoare logic are sound w.r.t. validity of Hoare triples.
    3. Completeness
      Completeness is impossible because a correct, complete and effective calculus would provide an enumeration of all nonterminating programs, which is impossible. Therefore: relative completeness w.r.t. oracle for validity of assertions. Proof of relative completeness for expressive assertion languages. Sketch of proof that first-order logic with arithmetic is expressive. Example of a non-expressive assertion language.
    4. Verification conditions
      Extension of IMP with loop invariants. Definition of functions wp (weakest precondition) and vc (verification condition) of type Com * Assn -> Assn. Proof of soundness of wp and vc with respect to Hoare logic. Statement of completeness (no proof).
  5. Type systems for IMP
    Static versus dynamic typing. TIMP: an extension of IMP with types bool and int. A type system for expressions and commands. A denotational semantics for expressions and a transition semantics for commands. Proof that the type system is correct w.r.t. the semantics: "TIMP is type safe". Extension 1: Polymorphism. Allow type variables in declarations. New version of type safety theorem using substitutions. Extensions 2: type inference. Compute missing declarations by using type checking rules as Prolog clauses.
  6. A compiler for IMP
    Code generation for a simple assembly language with instructions for assignment and (un)conditional jumps. Soundness and completeness theorems.
  7. Introdcution to domain theory
    Motivation: computable functions must be continuous. Discrete cpos. Product cpos. Thm An n-argument function is continuous iff it is continuous in each argument. Lambda-notation. The set of continuous functions as a cpo. Lifting. Disjoint sum. Application: denotational semantics of IMP.
  8. REC - A functional language
    Syntax of REC.
    1. Call by value: operational and denotational semantics; equivalence proof.
    2. Call by name: operational and denotational semantics.
    Compilers for the call-by-value and the call-by-name version of REC.
  9. Fixpoint induction
    Admissible predicates. The fixpoint induction theorem. Admissibility of inequations, equations, conjunction, disjunction and universal quantifiers. Counterexample for existential quantifiers. An example of fixpoint induction: conversion to tail recursion.
  10. Languages with higher types
    A functional language with numbers, products and functions. How to simulate mutual recursion by nested recursion. Becic's Theorem (without proof). The type system. Canonical terms. Operational and denotational semantics for eager evaluation (call-by-value). Agreement of the two semantics. Operational and denotational semantics for lazy evaluation. Full abstraction. Counterexample to full abstraction for HOREC.

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

Note: Two lectures hours each week are taught in English.

Voraussetzungen: Vordiplom

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.

Skript: keines

Literatur: Die Vorlesung orientiert sich stark an

G. Winskel: The Formal Semantics of Programming Languages. MIT Press.

Zwei deutsche Bücher, die Teile der Vorlesung abdecken: 
Apt und Olderog. Programmverifikation. Springer, 1994.
Eike Best. Semantik. Vieweg, 1995.

Sprechstunde: Mi 12:00-13:00 und nach Vereinbarung.

Tobias Nipkow, 4.11.98