INF220 - Programspesifikasjon
Contents on this web page
The course couples theory to practical programming in Magnolia.
Magnolia is a new programming language tightly integrating
specifications and code
with a foundation in institution theory.
It supports high integrity programming (reliable, robust, safe, secure)
by validating correctness and guarding every operation.
The course will cover topics like the following.
- Algebraic specifications as a means of defining API (application programmer interface) contracts.
- Institutions as a means of understanding modularisation, reuse and testing.
- Generic programming for reuse and correctness testing.
- Data invariants and congruences as a means for data abstraction and verification.
- 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,
most of it will be covered in the following handouts
(to be made available later).
- Magne Haveraaen: Magnolia Semantics - alpha release. 2018.
- Magne Haveraaen and Anya Bagge: Magnolia Tutorial - alpha release. 2018.
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.
Lecturer and course responsible: Magne Haveraaen
- 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.
See the official schedule, subject to change:
Teaching starts Monday August 20 2018 (week 34),
Teaching will be in the form of lectures, exercises and
time off for self studies.
The following teaching plan is very tentative and guaranteed to change.
- Mondays 1215 - 1400 in seminar room ???? HiB
- Fridays 1215 - 1400 in seminar room ???? HiB
The exam is planned for the end of November/beginning of December.
The exercises will be provided as the course evolves,
The course will probably be evaluated by an oral exam.
- 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)
Presentation of a practical problem to be solved using Magnolia
- Hackathon/Exercise set 5 (2 full days): solving the problem in Magnolia
- Student presentations: solution to the problem (compulsory)
- Data invariants and congruences
- Software development
- Pre-/post conditions
- Data abstraction
Sist oppdatert 2018-06-01 by