Syllabus for Programming Theory


A revised version of the syllabus is available.


  • 10 credits
  • Course code: 1DT034
  • Education cycle: Second cycle
  • Main field(s) of study and in-depth level: Computer Science A1N, Embedded Systems A1N
  • Grading system: Fail (U), Pass (3), Pass with credit (4), Pass with distinction (5)
  • Established: 2007-10-04
  • Established by: The Faculty Board of Science and Technology
  • Revised: 2007-11-06
  • Revised by: The Faculty Board of Science and Technology
  • Applies from: Autumn 2008
  • Entry requirements:

    120 credits with 30 credits in mathematics and 30 credits in computer science, including basic programming, data structures, and elementary logic.

  • Responsible department: Department of Information Technology

Learning outcomes

After completing this courses students will understand what it means to

write rigorous descriptions of implementations and specifications of programs,

verify programs, i.e. prove that the implementation of a program meets its specification, and

synthesise programs, i.e. to derive a correct program from a given specification.


The course will contain the following topics:

logical proofs, specification and correctness of programs, weakest preconditions, invariants, partial correctness, termination proofs, total correctness, and program synthesis.


Lectures and tutorials.


Written exam and assignments.

Syllabus Revisions

Reading list

Reading list

Applies from: Spring 2011

Some titles may be available electronically through the University library.

Last modified: 2022-04-26