INF220 - Program Specification

Contents on this web page

• Course outline and curriculum
• Teachers
• Schedule
• Semester plan
• Exercises
• Exam

Course outline and curriculum

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.

• C.A.R. Hoare: Proof of correctness of data representations. Acta Informatica 1(4):271-281 (1971). DOI 10.1007/BF00289507.
• James H. Morris Jr.: Types are Not Sets. POPL 1973:120-124. DOI 10.1145/512927.512938.
• Bertrand Meyer: Applying "Design by Contract". IEEE Computer 25(10): 40-51 (1992). Scan.
• Magne Haveraaen: Institutions, property-aware programming and testing. In Proceedings of the 2007 Symposium on Library-Centric Software Design (LCSD '07). 21-30 (2007). DOI 10.1145/1512762.1512765.
• Magne Haveraaen: Integrating specifications and code. Draft 2012.

Additional Reading Material

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

• David Gries: The Science of Programming. Springer 1981.
  Covers topic 1.
• Bertrand Meyer: Object-Oriented Software Construction, 2nd Edition Prentice-Hall 1997.
  Covers topic 2 and some of 3.
• Jacques Loeckx, Hans-Dieter Ehrich and Markus Wolf: Specification of abstract data types,
  Wiley Teubner, 1996, ISBN: 0-471-95067-x, 3-519-02115-3. Corrected chapter 10.
  Covers topic 4 and some of 5.
• Ole-Johan Dahl: Verifiable programming. Prentice Hall 1992.
  Covers topic 1 and much of 4.

Teachers

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

• Mondays 1415 - 1600 in seminar room 2104 HiB
• Tuesdays 1415 - 1600 in seminar room 2104 HiB
• Wednesdays 1215 - 1400 in seminar room 2104 HiB

Semester plan

34. Introduction: specifications for APIs and algorithms.
    Algebraic specifications: Interface, Interface morphisms, Algebra (theory)
    --
35. Algebraic specifications: Expressions (theory)
    Exercise set 1 (Set theory)
    Exercise set 1 (Set theory)
36. Algebraic specifications: Evaluation, Equational Specifications (theory)
    Magnolia specifications: Semigroup, Monoid, Group.
    Ralf Lämmel: Let’s specify a tiny information system! 101 companies
37. Algebraic specifications
38. Algebraic specifications
39. Institutions
40. Assertions
41. --
42. Pre-/post conditions
43. Pre-/post conditions and data invariants
44. Pre-/post conditions, data invariants and congruences
45. Data abstraction

Exercises

Exam