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: Mo 10:30-12:00 in N1070, Fr 9:30-11:00 in 0606

Beginn: 5.11.99

Übung: Di 13:15-14:45 in 1601
Übungsleitung: Gerwin Klein
Übungsschein: Einen Schein erhält, wer mindestens 40% der Punkte aus den Hausaufgaben und Programmieraufgaben erreicht und erfolgreich an der Semestralprüfung teilnimmt.

Prüfung:
Am 29.2.2000 findet statt der Übung die Semestralprüfung statt. Teilnahmeberechtigt sind alle Studierenden, die mindestens 40% der Punkte aus den Haus- und Programmieraufgaben erreicht haben. Wenn Sie an dieser mündlichen Prüfung teilnehmen möchten, melden Sie sich bitte bis spätestens 22.2.2000 per E-mail an Gerwin Klein <kleing@in.tum.de> an. Sie erhalten dann Antwort, ob Sie die Zulassungsvoraussetzungen zur Prüfung erfüllt haben.

Die Aufgabenblätter für die Zentralübung werden regelmäßig in der Vorlesung verteilt. 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: Eine einfache imperative Programmiersprache WHILE wird aus verschiedenen Blickwinkeln beschrieben und analysiert:

  1. Introduction
    The syntax of WHILE. Concrete vs abstract syntax. Evaluation of arithmetic and boolean expressions.
  2. Operational Semantics
    1. Big-step semantics
      The rules. Derivation trees. Lemma while b do s is equivalent to if b do s;while b do s else skip.
    2. Rule induction
      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.
    3. Small-step semantics
      The rules. Derivation sequences. Theorem: Agreement of big-step and small-step semantics.
    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. Local variables.
      4. 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.
    5. Application: a compiler for WHILE
      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.
  3. Type Systems
    Static vs dynamic typing.
    1. Types for WHILE.
      Merging the syntax of arithmetic and boolean expression. Types bool and int. Variable declarations.
    2. A monomorphic type system
      1. The type system
        Typing rules for expressions and statements. The need for semantics to talk about correctness of the type system.
      2. The semantics
        The need to separate booleans and integers. Semantics of expressions and statements. Theorem: Typed WHILE is type safe, i.e. type correct statements transform type correct states into type correct states.
    3. A polymorphic type system.
      1. Type checking
        Type variables. Typing rules and semantics unchanged! A rephrased type safety theorem based on substitutions for type variables: type correct statements guarantee type safe execution starting from any state that is type correct w.r.t. an instance of the polymorphic variable declarations.
      2. Type inference
        How to reconstruct the missing type declarations using type checking and unification, i.e. Prolog.
    A classification of various programming language according to static/dynamic and monomorphic/polymorphic.
  4. Denotational Semantics
    1. Inductive definitions and rule induction
      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.
    2. A denotational semantics based on sets
      The semantics of while-loops as a least fixpoint of a function which can be expressed by inference rules. Equivalence proof of denotational and operational semantics.
    3. Complete partial orders
      Definition of complete partial orders (cpos) and continuity. The Fixpoint Theorem. Discrete cpos, product cpos, function cpos, lifting.
    4. A cpo-based denotational semantics for While.
    5. Extensions of WHILE
      1. Local variables and procedures. Static scoping only.
      2. Exceptions and continuations.
      3. The Knaster-Tarski fixpoint theorem.
        Every monotone function on a complete lattice has a least fixpoint.
      4. Nondeterminism. Relational semantics already defined but too weak because it does not distinguish possible and guaranteed termination. Definition of the set of start states that guarantee termination using the Knaster-Tarski fixpoint theorem to obtain the least fixpoint of a monotone function (in the case of loops).
  5. Axiomatic Semantics (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. Completeness requires "expressive" language of arithmetic (beyond polynomials).
    8. Extensions of WHILE
      1. Nondeterminism
      2. Arrays
      3. Procedures: The problem. An adaption rule. A complete system based on a generalized consequence rule. (Soundness only sketched, completeness not proved.)
    9. Time complexity
      1. Exact execution times.
      2. Timed Hoare triples and their validity.
      3. Proof rules for timed Hoare triples.
  6. Operational semantics of functional languages
    1. A first-order language of recursion equations. Call by value and call by name semantics. Proof that termination of c-b-v implies termination of c-b-n.
    2. A higher-order language with call by value semantics.

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

Note: The lectures 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 und Literatur: Die Vorlesung orientiert sich stark an folgenden beiden Büchern

Tobias Nipkow, 24.1.2000