Skip to main content

DD2455 Theoretical Foundations of Object-Orientation 7.5 credits

This course covers the theoretical foundations of object-oriented programming. After a review of the principles of object-orientation, we consider a number of mathematical models of different aspects of object-oriented languages, including: abstract data types, concurrency, sequential correctness and type checking.

Course offering missing for current semester as well as for previous and coming semesters
Headings with content from the Course syllabus DD2455 (Spring 2009–) are denoted with an asterisk ( )

Content and learning outcomes

Course contents

  • A review of object-oriented themes, terminology, computational model, relationship to other programming paradigms, software lifecycle, new trends.
  • Principles of sequential program correctness. Operational semantics of sequential programs. Hoare’s logic and Floyd’s correctness analysis using labeled flowcharts. Programming by contract and Eiffel.
  • Abstract data types, signatures, equations, semantics. Objects as algebras. Correctness revisited.
  • Polymorphism. Inheritance and the subtype relation, flavours of polymorphism, type abstraction, existential types and information hiding.
  • Concurrency. Axioms for communicating processes, traces, interleaving semantics of concurrency.

Intended learning outcomes

The overall aim of the course is to provide an understanding of two advanced methods for ensuring object-oriented software quality, namely: (i) live sequence charts (LSCs) for requirements analysis, and (ii) invariant analysis of software code.

This understanding means that after the course you should be able to:

Critically assess an informal text-based software requirements document, identifying ambiguities, omissions and inconsistencies. Translate such a document into object-oriented requirements using a Noun/Verb/Relational-Phrase methodology. Construct a data dictionary, and relate this to the original requirements document using hypertext technology.

Identify, express in text, and formalise using LSCs the important use-cases in a requirements document. You should be able to distinguish between normal and exceptional scenarios.

Draw LSCs using the Play-Engine, given a pre-existing user interface model.

You should be able to organise your charts within a project, using the Play-Engine. You should also be able to modify the different components of a project with an understanding of the technical effects of any changes

Exercise a set of LSCs using the Play-Engine simulator to study their interaction, and how they co-operate to achieve the user requirements. You should understand what incomplete and inconsistent requirements are, and how to identify these by using simulation.

Translate a short piece (less than 20 lines) of object-oriented code into a flowchart. You should understand the meaning of a valid labelling of such a chart by logical assertions according to Floyd's invariant assertion method.

Construct a valid labelling of a flowchart by means of dragging a pre-condition forwards, or a postcondition backwards, and using basic logical transformations. You should be able to use your knowledge of programming to synthesize loop invariants and thus prove a program is mathematically correct with respect to a software requirement.

Understand the syntax of a simple sequential object-oriented programming language and be able to correctly add extra features to the syntax.

Understand the operational semantics of a simple sequential object-oriented programming language and be able to correctly add extra features to the semantics (for example garbage collection) that define the meaning of new syntactic features.

Understand the logic of a simple sequential object-oriented programming language and be able to explain the meaning of rules of inference.

Understand the concept of an abstract data type, how it relates to a class definition, and be able to define new simple data types.

Course disposition

No information inserted

Literature and preparations

Specific prerequisites

No information inserted

Recommended prerequisites

2D1350/2D1361/DD1361 Programming paradigms and 5B1928/SF1642 Logic.


No information inserted


A. Eliëns, Principles of Object-oriented Software Development, 2nd Edition, 2000, Addison-Wesley, ISBN 0-201-39856-7.

Examination and completion

If the course is discontinued, students may request to be examined during the following two academic years.

Grading scale

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


  • HEM1 - Home Work, 1.5 credits, grading scale: P, F
  • 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

Written examination (TEN1; 6 university credits), home work (HEM1; 1,5 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


Profile picture Karl Meinke

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.

Further information

Course web

No information inserted

Offered by

CSC/Computer Science

Main field of study

This course does not belong to any Main field of study.

Education cycle

Second cycle

Add-on studies

To be discussed with the course co-ordinator.


Karl Meinke, telefon: 790 6337, e-post:

Supplementary information

The course is not given 08/09.