Latest News
- 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.
Course Literature
Nielson
and Nielson
Semantics with Applications: An Appetizer
Springer-Verlag, 2007, ISBN: 978-1-84628-691-9
Available
from Kårbokhandeln at
the start of
the period.
In addition: some hand-written slides on axiomatic semantics and
verification condition generation (see outline,
part III).
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.
Course Structure
For formal reasons, the teaching is divided into lectures (F) and
tutorials
(Ö), but in fact there will be some kind of
"lektionsundervisning",
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.
Assignments
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).
Examination
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
bring
the course book, hand-outs and own lecture notes taken in class.
Note that you must be registered for the course in
order
to have the result of your exam reported.
Exam resits
Exam resits (sv. omtentor) are by mutual arrangement with the
lecturer.
Grading
The exam will be graded based on the intended learning outcomes of the
course. The successful student will be able to perform constructions
such as:
- 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
latter.
- 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
while loops.
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
content
and form of the education. It is formed at the beginning of the course.
Course Evaluation and Analysis
A course
evaluation is performed after the course to give input
for
improvements for later versions of the course. Here is the latest course
analysis
(in Swedish).