Till KTH:s startsida Till KTH:s startsida

Programsemantik och programanalys

Logga in till din kurswebb

Du är inte inloggad på KTH så innehållet är inte anpassat efter dina val.

Program Semantics and Analysis is a 6-point (högskolepoäng) course on the advanced level. It is coordinated together with its research-level version for doctoral students under the same name, but with course code FDD3457.

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 and prove such important properties like determinism and termination of program execution, equivalence of programs, correctness of translation of programs from one programming language into another, or that a program is correct. 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.

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.

The course is given in English. However, students can use Swedish when writing assignments and exams, and when communicating with the lecturer.

Lärare