Contents on this web page

• Course outline and curriculum
• Teachers
• Covid-19
• Schedule
• Semester plan
• Exercises
• Exam

Course outline and curriculum

1. 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.
2. Institutions as a framework for modularisation, reuse, specification and testing.
3. Semantic models: mathematical abstractions, bit patterns from hardware, abstract syntax trees and free constructions.
   (Partial) evaluators for free.
4. 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.
5. Cheap verification of generic code: free theorems, axiom inheritance, proof by testing.
6. Guarding (preconditions) against partiality.
   Free Constructions for error recovery.
7. Extended reuse by Syntactic Theory Functors (STFs) and Syntactic Model Functors (SMFs).

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: Notes for INF220 — Program Specification (Magnolia Edition). 2016-2019

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.

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.
• 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.

Teachers

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

Covid-19

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.

Schedule for lectures and seminar groups

• Mondays 1415 - 1600 in seminar room 302O1 HiB
• Wednesdays 1015 - 1200 in seminar room 302O1 HiB
• Thursdays 1215 - 1400 in seminar room 302O1 HiB (shifted from Tuesdays in week 37)

Semester plan

34. Axiom based testing in Java
35. Algebraic specification: interface, expression, model, assignment, evaluation, property specification, homomorphism (theory)
36. Exercise set 1 (Set theory)
    Exercise set 2 (Axiom based testing)
37. Monday: Exercises
    Algebraic specification: reuse (interface morphisms), satisfaction, institutions (theory)
38. Algebraic specifications: procedures, predicates (theory)
    Domain engineering (API, microservices, software product lines)
    Thursday: Exercise set 3 (Algebraic theory)
39. Introduction: Magnolia overview (language and library)
    Magnolia specifications: semigroup, monoid, group, lattice (pointless topology), sheaf, preorder.
    Algebraic specifications: constructing algebras (products, subalgebras, quotients), specification expressiveness (theory)
    Exercise set 4
40. 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)
41. Hackathon/Exercise set 6 (preferably several full days): solving the domain engineering problems in Magnolia
42. TBD
43. Student presentations: solution to the problems (compulsory)
44. Assertions, pre-/post conditions
45. Software development
46. Data abstraction
47. TBD

Exercises

Exam