- Algebraic specifications for discovering and defining API contracts.
This process is called
*Domain Engineering*.

Good API design is central for domain specific languages, software product lines, microservices and web services in general. - Institutions as a framework for modularisation, reuse, specification and testing.
- Semantic models: mathematical abstractions, bit patterns from hardware, abstract syntax trees and free constructions.

(Partial) evaluators for free. - Generic programming for code reuse and remodelling of axioms.
- Data construction by data structures, data invariants and congruences (generated by and paritioned by clauses).

A basis for a high level theory of exploits (vulnerabilities). - Assertions (pre-/postconditions) as a means for understanding algorithms.

- Data construction by data structures, data invariants and congruences (generated by and paritioned by clauses).
- Cheap verification of generic code: free theorems, axiom inheritance, proof by testing.
- Guarding (preconditions) against partiality.

Free Constructions for error recovery. - Extended reuse by Syntactic Theory Functors (STFs) and Syntactic Model Functors (SMFs).

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

- Magne Haveraaen: Notes for INF220 — Program Specification (Magnolia Edition). 2016-2019
- Dines Bjørner: Domain Science and Engineering — A Foundation for Software Development.
*Monographs in Theoretical Computer Science. An EATCS Series. Springer.*2021.

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

- Anya Helene Bagge and Magne Haveraaen: Specification of Generic APIs, or: Why Algebraic May Be Better Than Pre/Post.
*Proceedings of the 2014 ACM SIGAda Annual Conference on High Integrity Language Technology (HILT14)*71-80 (2014). DOI 10.1145/2663171.2663183. - 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. - C.A.R. Hoare: Proof of correctness of data representations.
*Acta Informatica*1(4):271-281 (1971). DOI 10.1007/BF00289507. - Bertrand Meyer: Applying "Design by Contract".
*IEEE Computer*25(10): 40-51 (1992). DOI 10.1109/2.161279. - James H. Morris Jr.: Types are Not Sets.
*POPL*1973:120-124. DOI 10.1145/512927.512938.

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. - Barbara Liskov and John Guttag:
*Abstraction and Specification in Program Development*, MIT Press, 1986, ISBN: 978-0262121125. - John V. Guttag, James J. Horning, Stephen J. Garland, Kevin D. Jones, A. Modet, Jeannette M. Wing:
*Larch: Languages and Tools for Formal Specification*. Texts and Monographs in Computer Science, Springer 1993, ISBN 978-1-4612-7636-4, pp. 1-156. DOI 10.1007/978-1-4612-2704-5 - Ole-Johan Dahl:
*Verifiable programming*. Prentice Hall 1992. - David Gries:
*The Science of Programming*. Springer 1981. - Bertrand Meyer:
*Object-Oriented Software Construction*, 2nd Edition Prentice-Hall 1997.

Teaching assistant: TBD

Guest appearance: Dines Bjørner on Domain Engineering

The participants are adviced to organise study groups for discussing the topics of the course and assist each other in solving the exercises.

UiB guidelines for keeping safe.

- Stay at home and get tested if you are experiencing respiratiory symptoms
- Clean your hands with sanitiser gel before entering the teaching areas (also wipe your desk before and after using it)
- Keep a minimum of 1 meter distance to everyone
- When entering: Keep in line and keep distance. Fill row by row as you enter. When leaving: leave the room row by row. Those who are closest to the door should leave first.
- Please register in Studentweb for the courses you attend to help us provide you with information in the case of identified contamination in your group.

I will try to stream the lectures for those who are in quarantine. See MittUiB for details.

- Tuesdays 1415 - 1600 in seminar room 302O1 HiB
- Wednesdays 1015 - 1200 in seminar room 302O1 HiB
- Fridays 0815 - 1000 in seminar room 302O1 HiB

- Domain engineering beginnings
- Algebraic specification: interface, expression, model, assignment, evaluation, property specification, homomorphism (theory)
- Exercise set 1 (Set theory)

Exercise set 2 (Axiom based testing) - Monday: Exercises

Algebraic specification: reuse (interface morphisms), satisfaction, institutions (theory) - Algebraic specifications: procedures, predicates, composition of homomorphisms/interface morphisms, generated/free/initial algebras, evaluation homomorphism (theory)

Thursday: Exercise set 1 & 2 - Introduction: Magnolia overview (language and library)

Magnolia specifications: semigroup, monoid, group, lattice (pointless topology), sheaf, preorder.

Domain engineering (API, microservices, software product lines)

Algebraic specifications: constructing algebras (products, subalgebras, quotients), specification expressiveness (theory)

Thursday: Exercise set 3 (Algebraic theory)

Exercise set 4 - Generic programming (theory, Magnolia)

Data structures: products, powers, data invariants, congruences

Cheap verification

Presentation of three domain engineering problems to be solved using Magnolia (compulsory assignment)

Exercise set 5 (Installing Magnolia, Magnolia tutorial) - Hackathon/Exercise set 6 (preferably several full days): solving the domain engineering problems in Magnolia
- TBD
- Student presentations: solution to the problems (compulsory)
- Assertions, pre-/post conditions
- Software development
- Data abstraction
- TBD

Last updated 2021-08-20 by Magne Haveraaen