- Algebraic specifications as a means of defining API (application programmer interface) contracts.
- Institutions as a means of understanding modularisation, reuse and testing.
- Data invariants and congruences as a means for data abstraction.
- Assertions as a means of understanding algorithms.
- Pre-/post-conditions as a means of understanding methods.

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.

- Magne Haveraaen: Magnolia Semantics - alpha release. 2015.
- Magne Haveraaen and Anya Bagge: Magnolia Tutorial - alpha release. 2015.
- 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. - 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. - C.A.R. Hoare: Proof of correctness of data representations.
*Acta Informatica*1(4):271-281 (1971). DOI 10.1007/BF00289507.

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

- 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 1 and some of 2 and 3. - Ole-Johan Dahl: Verifiable programming. Prentice Hall 1992.

Covers topic 1, 3 and much of 4. - David Gries: The Science of Programming. Springer 1981.

Covers topic 4. -
Bertrand Meyer: Object-Oriented Software Construction, 2nd Edition Prentice-Hall 1997.

Covers topic 4 and some of 5.

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.

- Tuesdays 1415 - 1600 in seminar room 2104 HiB
- Wednesdays 1215 - 1600 in seminar room 2104 HiB

- Introduction: Magnolia overview (language and library)

Algebraic specifications: Interface, Algebra (theory)

Algebraic specifications: Expressions (theory) - Exercise set 1 (Set theory)

Algebraic specifications: Evaluation, Equational Specifications (theory)

Exercise set 2 (Installing Magnolia) - Algebraic specifications: module reuse (theory, Magnolia)

Magnolia specifications: Semigroup, Monoid, Group.

Exercise set 3 (Magnolia Tutorial) - Algebraic specifications (expressiveness): API vs logic (theory)

Magnolia specifications: preorders, lattices.

Exercise set 4 - Algebraic specifications: institutions (theory, Magnolia)

Ralf Lämmel: 101 companies - Hackathon/Exercise set 5 (2 full days): 101 companies in Magnolia
- Student presentations: 101 companies solved
- Data invariants and congruences
- TBD
- Assertions
- TBD
- Software development
- Pre-/post conditions
- TBD
- Data abstraction

Sist oppdatert 2015-07-02 by Magne Haveraaen