DD2454 Semantics for Programming Languages

Lectures & Tutorials

Lecture 1.

• Introduction: semantics of programming languages: what is semantics, why it is interesting and important, what the course is all about, its syllabus.
• Administration: course web page, structure of the course, evaluation, course leader, literature, course board, etc.

  Part I. Operational Semantics
  

Lecture 2. Ch. 2.1-2.4.

• Syntax of the imperative toy programming language IMP.
• Operational semantics of the arithmetic expressions of IMP, evaluation procedure.
• Operational semantics of the boolean expressions and the commands of IMP.

Exercises:

• Evaluate (4 × X) + 3  in a state s such that s(X) = 2.
• What guarantees termination of the evaluation procedure?

Lecture 3. Ch. 2.5.

Exercises:

• Derive the result of evaluating X := 0; while 0<=X do X := X -1.
• Suggest an evaluation strategy.
• Show the equivalence:  if b then c1 else c2  ~ if ¬b then c2 else c1.
• Proposition 2.8: Show the equivalence  w ~ w'  where  w = while b do c  and  w' = if b then c;w else skip.
• Exercise 2.7: Derive the result of evaluating while true do skip  in a state s. Problem?!
• What is the operational semantics of non-terminating programs?

Lecture 4. Ch. 2.6.

• A small-step operational semantics for IMP.
• Adding read and write commands to the language.
• An abstract machine semantics for IMP.

Exercises:

• Derive the configuration graph of  while true do skip  under the small-step semantics.
• The same for X := 0; while 0<=X do X := 1-X.
• Execute while true do skip;skip in both small-step and abstract machine semantics. Compare.

Lectures 5 and 6. Ch. 3, Ch. 4.

• Mathematical induction, Course-of-values induction.
• Well-founded induction.
• Structural induction.
• Rule Induction.

Exercises:

• Show by mathematical induction on s(X) that  while 0<=X do X := X -1  terminates for all states s such that s(X)=>0.
• Theorem 3.10: Euclid terminates from all states assigning positive values to X and Y.
• Proposition 3.3: Evaluation of arithmetic expressions is deterministic.
• Exercise 3.4: Show termination of evaluation of arithmetic expressions.
• Exercise 3.5: Show evaluation of boolean expressions terminates and is deterministic.
• Theorem: The large-step and the small-step operational semantics of IMP are equivalent.
• Theorem 3.11: Execution of commands is deterministic

  Part II. Denotational Semantics

Lecture 7. Ch. 5.1-5.2.

• Operational semantics: Summary
• Why denotational semantics?
• Denotational semantics of IMP.

Lecture 8. Ch. 5.4.

• Introduction to fixed point theory.
• Iterative computation of fixed points.

Exercises:

• Compute iteratively the denotation of while ~(X=0) do X := X -2.

Lecture 9. Ch. 5.3.

• Equivalence of the operational and denotational semantics of IMP.
  

Part III. Axiomatic Semantics and Program Verification

Lecture 10. Ch. 6.1, 6.4.

· Introduction to axiomatic semantics and program verification.

· Axiomatic semantics of IMP: the rules.

· Some simple program verifications.

Exercises:  Derive the Hoare triples:

· {X<0} if 0<=X then X:=X+1 else X:=1 {X=1}.

· {X<0} while ~(X=0) do X:=X-1 {false}.

· {true} while ~(X=0) do X:=X-1 {X=0}.

Lecture 11. Ch. 6.6.

· Program verification: pro's and con's.

· Proof tableaux.

· Verifying programs with while loops.

· Loop invariants.

Exercises:  Specify and verify the programs:

· computing the maximum of two numbers with if X<=Y then Z:=Y else Z:=X.

· checking whether a non-negative integer is even or odd with  while 2<=X do X:=X-2.

· computing the gcd of two positive integers with Euclid.

Lecture 12.

· Solving the midterm assignment in class.

· Weakest preconditions and semi-automatic program verification.

Lecture 13. Ch. 6.2, 6.3, 6.5.

· Syntax and semantics of the assertion language.

· Semantics of Hoare triples (i.e., partial correctness assertions).

· Soundness of the axiomatic semantics.

Part IV. Recursion Equations and Domain Theory

Lecture 14. Ch. 9.1, 9.2, 9.5.

· The applicative programming language REC.

· Evaluation strategies: call-by-value, call-by-name.

· Operational semantics of REC for call-by-value.

· Operational semantics of REC for call-by-name.

Exercises:

· Evaluate pow(2,1) under the declaration pow(x,y) = if y then 1 else x x pow(x,y-1)

· Suggest a small-step operational semantics for call-by-value evaluation.

· Evaluate pow(2,1) under your small-step semantics.

Lecture 15. Ch. 9.3, 9.6, 8.1, 8.3

· Denotational semantics of REC.

· Domain Theory