INF220 - Programspesifikasjon
Autumn 2012
Contents on this web page
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).
- Assertions as a means of understanding algorithms.
- Pre-/post-conditions as a means of understanding methods.
- Data invariants and congruences as a means of understanding data abstraction.
- Algebraic specifications as a means of defining API contracts.
- Institutions as a means of understanding modularisation, reuse and testing.
Reading Material
There is no specific text book, and the curriculum consists of
all lectures, notes, handouts, exercises, and related course material.
The following is a start on the reading list for the course.
- 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.
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.
- Mondays 1415 - 1600 in seminar room 2104 HiB
- Tuesdays 1415 - 1600 in seminar room 2104 HiB (interleaved with inf328)
- Wednesdays 1215 - 1400 in seminar room 2104 HiB
Teaching starts Monday August 20 2012 (week 34),
Teaching will be in the form of lectures, exercises and
time off for self studies.
The teaching is planned to cover the following topics,
tentatively listed by week no.
- Introduction, assertions for a sorting algorithm.
- Assertions
- Pre-/post conditions
- Pre-/post conditions and data invariants
- Pre-/post conditions, data invariants and congruences
- Data abstraction
- Algebraic specifications
- Algebraic specifications
- Algebraic specifications
- Algebraic specifications
- Institutions
The exam is planned for the end of November/beginning of December.
The exercises will be provided as the course evolves.
The course will be evaluated by an oral exam.
Sist oppdatert 2013-06-11 by
Magne Haveraaen