INF220 - Program Specification

INF220 - Programspesifikasjon

Autumn 2013

Contents on this web page

Course outline and curriculum

The course this semester has a pragmatic approach to specification, i.e., the theory is tightly coupled to programming. The course will cover the following topics (as time permits).
  1. Algebraic specifications as a means of defining API contracts.
  2. Institutions as a means of understanding modularisation, reuse and testing.
  3. Data invariants and congruences as a means of understanding data abstraction.
  4. Assertions as a means of understanding algorithms.
  5. Pre-/post-conditions as a means of understanding methods.

Reading Material

There is no specific text book, and the curriculum consists of all lectures, notes, handouts, exercises, and related course material. The following supplementary reading material gives an idea about the course contents.

Additional Reading Material

For those especially interested in reading up on the background material, the following (classical) books are recommended.


Lecturer and course responsible: Magne Haveraaen
Teaching assistant: TBD

The participants are adviced to organise study groups for discussing the topics of the course and assist each other in solving the exercises.

Schedule for lectures and seminar groups

Teaching starts Monday August 19 2013 (week 34), Teaching will be in the form of lectures, exercises and time off for self studies.

Semester plan

The teaching is planned to cover the following topics, tentatively listed by week no.
  1. Introduction: specifications for APIs and algorithms.
    Algebraic specifications: Interface, Interface morphisms, Algebra (theory)
  2. Algebraic specifications: Expressions (theory)
    Exercise set 1 (Set theory)
    Exercise set 1 (Set theory)
  3. Algebraic specifications: Evaluation, Equational Specifications (theory)
    Magnolia specifications: Semigroup, Monoid, Group.
    Ralf Lämmel: Let’s specify a tiny information system! 101 companies
  4. Algebraic specifications
  5. Algebraic specifications
  6. Institutions
  7. Assertions
  8. --
  9. Pre-/post conditions
  10. Pre-/post conditions and data invariants
  11. Pre-/post conditions, data invariants and congruences
  12. Data abstraction
The exam is planned for the end of November/beginning of December.


The exercises will be provided as the course evolves, check miside.


The course will be evaluated by an oral exam.
Sist oppdatert 2013-09-04 by Magne Haveraaen