Content

In this course, you will learn how to formally attach meaning to the syntax of a programming language, i.e. how to specify in a mathematically rigorous way what a program in your programming language actually does. We will then also explore how a formal semantics gives rise to techniques for program verification and analysis. The following concepts will be discussed:

• different types of formal semantics: big-step, small-step, denotational
• correctness of compilers
• type systems
• simple program analysis and modification (guaranteed initialisation analysis, constant folding, liveness)
• weakest precondition reasoning and the Hoare calculus
• partial and total correctness of programs
• abstract interpretation
• if we have time: outlook on some advanced topics such as parallelism, nondeterminism, probabilistic programming, mutable state and separation logic

A special feature in this coarse is that it is very hands-on: all concepts mentioned above will not merely be shown on paper, but constructed and explored in the proof assistant Isabelle (to be more precise: Isabelle/HOL) and a simple imperative toy programming language called IMP. No prior knowledge of Isabelle is required; the course also serves as a gentle introduction to Isabelle as a side effect.

Prerequisites

There are no hard prerequisites for this course, However, in order to do well in this course and enjoy it, fundamental knowledge of and a healthy interest in the following is strongly recommended:

• basic propositional and predicate logic
• basic discrete mathematics (sets, relations, orders)
• functional programming (since Isabelle/HOL shares many similarities with functional programming)

All of these are typically taught in undergraduate computer science courses.

Recommended literature

This course is based on the book Concrete Semantics with Isabelle/HOL by Nipkow & Klein. A free PDF version of the book and supplementary material are available on the authors' website.

Sneak preview

If you just want to get a feeling for the kinds of things we will be doing in this course: the following is the definition of the syntax of the IMP programming language in Isabelle/HOL. This is a simple Turing-complete imperative programming language that is similar to the register machines you may be familiar with from your undergraduate theoretical computer science course.

type_synonym vname = string
  
(* arithmetic expressions: literals, variables, addition *)
datatype aexp = N int | V vname | Plus aexp aexp
  
(* boolean expressions: literals, negation, conjunction, comparison *)
datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
  
(* programs with assignments, conditionals, and while loops *)
datatype
  com = SKIP 
      | Assign vname aexp       ("_ ::= _" [1000, 61] 61)
      | Seq    com  com         ("_;;/ _"  [60, 61] 60)
      | If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
      | While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)

We can now assign a meaning to this language using a big-step semantics. We write (c, s) ⇒ s' for the statement "starting with the initial state s, the program c terminates, and after its terminations the resulting state is s'".

type_synonym val = int
type_synonym state = "vname ⇒ val"
  
fun aval :: "aexp ⇒ state ⇒ val" where
"aval (N n) s = n" |
"aval (V x) s = s x" |
"aval (Plus a1 a2) s = aval a1 s + aval a2 s"
  
fun bval :: "bexp ⇒ state ⇒ bool" where
"bval (Bc v) s = v" |
"bval (Not b) s = (¬ bval b s)" |
"bval (And b1 b2) s = (bval b1 s ∧ bval b2 s)" |
"bval (Less a1 a2) s = (aval a1 s < aval a2 s)"
  
inductive
  big_step :: "com × state ⇒ state ⇒ bool" (infix "⇒" 55)
where
  Skip:       "(SKIP,s) ⇒ s" |
  Assign:     "(x ::= a,s) ⇒ s(x := aval a s)" |
  Seq:        "⟦ (c1,s1) ⇒ s2;  (c2,s2) ⇒ s3 ⟧ ⟹ (c1;;c2, s1) ⇒ s3" |
  IfTrue:     "⟦ bval b s;  (c1,s) ⇒ t ⟧ ⟹ (IF b THEN c1 ELSE c2, s) ⇒ t" |
  IfFalse:    "⟦ ¬bval b s;  (c2,s) ⇒ t ⟧ ⟹ (IF b THEN c1 ELSE c2, s) ⇒ t" |
  WhileFalse: "¬bval b s ⟹ (WHILE b DO c,s) ⇒ s" |
  WhileTrue:  "⟦ bval b s1;  (c,s1) ⇒ s2;  (WHILE b DO c, s2) ⇒ s3 ⟧ ⟹ (WHILE b DO c, s1) ⇒ s3"

As an example, here is a program which, given an integer x, computes the number 1 + 2 + … + x and stores the result in the variable y (assuming we initially have y = 0):

definition myprogram :: com where
  "myprogram =
     WHILE Less (N 0) (V ''x'')
     DO (''y'' ::= Plus (V ''y'') (V ''x'') ;;
         ''x'' ::= Plus (V ''x'') (N (-1)))"

We can now prove the correctness of this program in terms of our semantics above:

lemma
  assumes "s ''y'' = 0"
  shows   "∃s'. (myprogram, s) ⇒ s' ∧ s' ''y'' = (∑i=1..s ''x''. i)"

Or, more compactly, as a Hoare triple:

lemma "⊢ {λs. s ''x'' = n ∧ s ''y'' = 0}
         myprogram
         {λs. s ''y'' = (∑i=1..n. i)}"