Semantics for Programming Languages, semant08
DD2454 Semantics for Programming Languages
- If you haven't already done this in class, please print and fill
in the following anonymous course evaluation
sheet and put it in my mailbox.
Semantics with Applications: An Appetizer
Springer-Verlag, 2007, ISBN: 978-1-84628-691-9
the start of
In addition: some hand-written slides on axiomatic semantics and
verification condition generation (see outline
Additional reading for the curious student:
- a paper by Freund and Mitchell
formalizing the Java
Virtual Machine and Language, thus providing an abstract machine
semantics for the Java bytecode language JVML.
For formal reasons, the teaching is divided into lectures (F) and
(Ö), but in fact there will be some kind of
where theory and examples are mixed.
Here is the course schedule
. The following course outline
will follow the material already covered, and suggest reading and
exercises, both based on the course book.
The assignments will typically consist of a number of exercises taken
from the textbook. They will be checked in class by peer reviewing,
with the help of solutions provided by the lecturer, and be collected
by the lecturer. At least 60% of all assignments have to be handed in
as a prerequisite to admission to the final exam. Each assignment
handed in on time will contribute a bonus point for the final exam
(which will consist of ca. 30 points).
The requirement for the course is a pass on the written exam. The grade
will be the grade obtained at
the exam. You're allowed to
the course book, hand-outs and own lecture notes taken in class.
Note that you must be registered for the course in
to have the result of your exam reported.
Exam resits (sv. omtentor) are by mutual arrangement with the
The exam will be graded based on the intended learning outcomes of the
course. The successful student will be able to perform constructions
- Construct the state space of a program as a basis for program
behaviour analysis through state space exploration.
- Translate programs to abstract machine code, and execute the
- Compute the denotation of a program.
- As above, but in abstract domains.
- Extend a programming language with new language features, and
extend its semantics and abstract machine implementations accordingly.
- Suggest and justify program transformations, supported by a
suitable program analysis.
- Specify and verify programs in Hoare logic.
- Generate verification conditions from a program with annotated
As well as be able to formally establish results such as:
- 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.
- Show properties of a given semantics.
For passing the course, a student has to demonstrate proficiency with
problems of the first type; for the highest grade he/she has to be
equally proficient at the remaining types of problems.
Bonus points will be taken into account, namely one bonus point per
homework assignment handed in on time.
Course Board (sv. Kursnämnd)
A course board
is a formal way for students to influence the
and form of the education. It is formed at the beginning of the course.
Course Evaluation and Analysis
is performed after the course to give input
improvements for later versions of the course. Here is the latest course