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 (application programmer interface) contracts.
2. Institutions as a means of understanding modularisation, reuse and testing.
3. Generic programming for reuse and correctness testing.
4. Data invariants and congruences as a means for data abstraction and verification.
5. Assertions as a means of understanding algorithms.
6. Pre-/post-conditions as a means of understanding methods.

Reading Material

The curriculum consists of all lectures, notes, handouts, exercises, and related course material, most of it will be covered in the following handouts (to be made available later — check mittuib).

• Magne Haveraaen: Magnolia Semantics - alpha release. 2019.
• Magne Haveraaen and Anya Bagge: Magnolia Tutorial - alpha release. 2019.

The following supplementary reading material gives an idea about the course contents.

• Magne Haveraaen: Domain Engineering the Magnolia Way. Proceedings of Ershov Informatics Conference 2017 (PSI '17). 196-210 (2017). DOI 10.1007/978-3-319-74313-4_15.
• Magne Haveraaen: Institutions, property-aware programming and testing. 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.

Additional Reading Material

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.

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 1215 - 1400 in seminar room 405O2 HiB (the aquarium)
• Tuesdays 1015 - 1200 in seminar room 405O2 HiB (the aquarium)
• Wednesdays 1015 - 1200 in seminar room 405O2 HiB (the aquarium)

Semester plan

34. Introduction
    Magnolia overview (language and library), algebraic specifications: interface, algebra (theory)
    Algebraic specifications: expressions, evaluation (theory)
35. Exercise set 1 (Set theory)
    Exercise set 2 (Installing Magnolia)
    Algebraic specifications: specification logics (theory)
36. Algebraic specifications: module reuse (theory, Magnolia)
    Magnolia specifications: semigroup, monoid, group.
    Exercise set 3 (Magnolia tutorial)
37. Algebraic specifications (expressiveness): API vs logic (theory)
    Magnolia specifications: preorders, lattices, sheaves.
    Exercise set 4
38. Algebraic specifications: institutions (theory, Magnolia)
    Presentation of a practical problem to be solved using Magnolia
39. Hackathon/Exercise set 5 (2 full days): solving the problem in Magnolia
40. Student presentations: solution to the problem (compulsory)
41. Tuples, data invariants and congruences
42. TBD
43. TBD
44. Assertions, pre-/post conditions
45. Software development
46. TBD
47. Data abstraction

Exercises

Exam