DD2454 Semantics for Programming Languages 6.0 credits

Semantik för programspråk

To give a semantics for a programming language means to give a precise definition of the behaviour of programs written in this language. Only when the semantics of the language has been fixed, one can go about to prove such important properties like determinism and termination, equivalence of constructs, or that a given program meets its specification. Different semantic styles have been developed for different purposes, depending on the level of detail needed for the particular task. The most important ones are: operational semantics, denotational semantics and axiomatic semantics.

Offering and execution

Course offering missing for current semester as well as for previous and coming semesters

Course information

Content and learning outcomes

Course contents *

1. Operational Semantics: big-step semantics, small-step semantics and abstract machine semantics for the simple imperative language IMP.

2. Analysing IMP programs: state space exploration, termination, equivalence. Determinism of IMP.

3. Denotational Semantics for IMP. Fixed Point Theory. Relation with big-step operational semantics.

4. Axiomatic Semantics for IMP. Program Verification. Computing weakest preconditions.

5. Operational and denotational semantics for the simple declarative language REC. Domain Theory.

Intended learning outcomes *

The overall aim of the course is to study the main semantic styles used for capturing the meaning of programs in a formal way, compare their strengths and weaknesses, and analyze how they can be used for establishing important properties of programming languages, concrete programs, and transformations on programs. A secondary goal is to learn the theories and proof techniques on which such semantic investigations are based.

After the course, the successful student will be able to perform the following constructions:

  • construct the state space of a program as a basis for program behaviour analysis through state space exploration;
  • compute the denotation of a program;
  • extend a programming language with new constructs, and extend its semantics accordingly;
  • specify and verify programs in Hoare logic,
  • formally relate different semantic styles;
  • prove language properties such as determinism and termination;
  • show correctness of a given program transformation by proving equivalence of the original and the transformed program.

For passing the course, a student has to demonstrate proficiency with problems of type 1-4; for the highest grade he/she has to be equally proficient at the remaining types of problems.

Course Disposition

No information inserted

Literature and preparations

Specific prerequisites *

No information inserted

Recommended prerequisites

No information inserted

Equipment

No information inserted

Literature

Nielson and Nielson "Semantics with Applications: An Appetizer", Springer-Verlag, 2007, ISBN: 978-1-84628-691-9.

Examination and completion

Grading scale *

A, B, C, D, E, FX, F

Examination *

  • TEN1 - Examination, 6.0 credits, Grading scale: A, B, C, D, E, FX, F

Based on recommendation from KTH’s coordinator for disabilities, the examiner will decide how to adapt an examination for students with documented disability.

The examiner may apply another examination format when re-examining individual students.

Other requirements for final grade *

Examination (TEN1; 6 university credits)

Opportunity to complete the requirements via supplementary examination

No information inserted

Opportunity to raise an approved grade via renewed examination

No information inserted

Examiner

Dilian Gurov

Further information

Course web

No information inserted

Offered by

CSC/Computer Science

Main field of study *

No information inserted

Education cycle *

Second cycle

Add-on studies

No information inserted

Contact

Dilian Gurov, tel: 790 8198, e-post: dilian@csc.kth.se

Ethical approach *

  • All members of a group are responsible for the group's work.
  • In any assessment, every student shall honestly disclose any help received and sources used.
  • In an oral assessment, every student shall be able to present and answer questions about the entire assignment and solution.

Supplementary information

Lectures: 20 h
Tutorials: 10 h.

The course is given every second year.

Registration for examination is required.