CSEN 920

4 lecture hours


4  ECTS credits

Semantics of Programing Languages (Elective for MET)

Abstract

  • Semantics of Programming Languages deals with building a mathematical model to describe the meaning of programs. The purpose is to clearly understand and reason about a program's behavior, which is essential
    to all kinds of analysis, verification, and transformation (e.g., compiling) of programs, but also fundamental for a deeper understanding of the subtleties of programming.

    In this class we will introduce and use a minimal imperative programming language called IMP (and, if time permits, a likewise minimal recursive programming language called REC) as an example case to define its meaning using the three major semantic formalisms: Operational, denotational, and axiomatic semantics.

    Operational semantics describes the meaning of programs by defining how they execute on an abstract machine. It is most useful for understanding structure and implementation of a language. Denotational semantics describe the meaning of a program in terms of partial functions on states. It is most useful for comparison and translation of different programming languages.

    Axiomatic semantics describe the meaning of programs in terms of logical assertions. It is used to elegantly prove correctness of a program.

    There are no immediate prerequisites, all necessary background will be provided. However, fundamental understanding of logics (conjunction, disjunction, implication, quantification) and an appreciation of clever, abstract, thought and insight will help to enjoy this class.

Outline

    • Basics of set theory and induction
    • The operational semantics of IMP (evaluation of expressions, execution of commands, proofs, alternatives)
    • Inductive definitions and rule induction
    • The denotational semantics of IMP (motivation, partial functions on states, fixpoint semantics)
    • The axiomatic semantics of IMP (assertion language, Hoare rules, partial correctness proofs)
    • Basic domain theory
    • Recursive equations and the language REC
    • Operational semantics of REC (call-by-name, call-by-value)

Objectives

    • Understanding operational semantics and its basics and being able to prove program results through proof trees.
    • Understanding denotational semantics and its background
    • Understanding axiomatic semantics and proving (partial) correctness of programs trough Hoare triples and proof rules

Course Editions

RenewSession