Contents on this web page

• Course content and curriculum
• Teachers
• Schedule
• Semester plan
• Exam

Course content and curriculum

The course presents a theory for the design and reuse of software components. The focus is on APIs (signatures/interfaces) with property specifications, and studies how this gives a full theory of generic code reuse. The framework provides a close match to computer hardware, including multicore, parallel computers, GPUs and emerging energy efficient hardware architctures.

Property specifications can be formally verified using tools, ensuring software correctness. A timely question is if this is how to tame generative programming, like GitHub's copilot and Chat-GPT. Such tools generate seemingly good code, but there is no guarantee the provided code is relevant, correct or safe.

The course's theory is illustrated with practical software development in Magnolia. Magnolia is an experimental programming language tightly integrating property specifications and program code. Compiled code can be run as command line applications or interpreted as, e.g., microservices. The language design supports high integrity programming (reliable, robust, safe, secure) by validating correctness and guarding every operation.

The course looks into topics like the following.

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.
   The setting gives us evaluators for free.
4. Generic programming for code reuse and translation of property specifications.
   • Data construction by data structures, data invariants and congruences (related to generated by and partitioned by clauses – known as encapsulation in object-oriented programming).
     This also gives a high level perspective on vulnerabilities (security exploits).
   • Assertions (pre-/postconditions) as a means for understanding algorithms.
5. Cheap verification of generic code: free theorems, property inheritance, proof by testing.
6. Guarding (preconditions) against partiality.
   Which gives free constructions for error recovery.
7. Extended reuse by Syntactic Theory Functors (STFs) and Syntactic Model Functors (SMFs).
8. Green computing (sustainable computing): programming models and techniques that support more efficient use of hardware, thus cutting the energy cost for computations. This is important for mobile computing where batteries capacity is limited. It is also important for large scale computing, where significant amounts of electricity can be saved.

Reading Material

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

• Magne Haveraaen: Notes for INF220 — Program Specification (Magnolia Edition). 2016-2023

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
• 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
• James H. Morris Jr.: Types are Not Sets. POPL 1973:120-124. DOI 10.1145/512927.512938
• 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
• Magne Haveraaen: Axiom Based Testing for Fun and Pedagogy. In: Cerone A., Roggenbach M. (eds) Formal Methods – Fun for Everybody. FMFun 2019. Communications in Computer and Information Science, vol 1301. Springer, Cham. DOI 10.1007/978-3-030-71374-4_2
• Bertrand Meyer: Applying "Design by Contract". IEEE Computer 25(10): 40-51 (1992). DOI 10.1109/2.161279
• 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 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

Lecturer and course responsible: Magne Haveraaen
Teaching assistant: Sander Wiig

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

See the official schedule, which may be subject to change:

• Mondays 1215 - 1400 in seminar room Rips 302O1 HiB
• Tuesdays 1215 - 1400 in seminar room Rips 302O1 HiB
• Thursdays 0815 - 1000 in seminar room Rips 302O1 HiB (exercise class)

The HiB building (Høyteknologisenteret i Bergen) is Thormøhlensgt 55, 5008 Bergen. The room is in datablokken, the taller of the two towers (to the right of the main entrance).

Semester plan

The following teaching plan is tentative and will change.

34. Foundations 1: interface, expression, model, assignment, evaluation — generative AI and binary search
    Exercise set 1 (Set theory)
35. Foundations 2: property specification (EL, CEL), satisfaction.
    Exercise set 1 (Set theory)
36. Foundations 3: property specification (BL), reuse (inclusion morphisms), institutions;
    Exercise set 2 (Specification theory)
37. Foundations 4: satisfaction, reuse (interface morphisms), institutions; models Mod and theories Th
    Exercise set 3 (Installing Magnolia, Magnolia tutorial)
38. Magnolia overview (language and library); Homomorphisms
    Examples: semigroup, monoid, group, semiring, ring — possibly lattice (pointless topology), sheaf, preorder.
    Exercise set 4 (Institutions)
39. Foundations 5: expression algebras and evaluation homomorphisms, generated/free/initial algebras, homomorphic image algebra and property preservation
    Exercise set 5 (Property testing)
40. Foundations 6: constructing algebras (subalgebras, products/powers, quotients), property preservation and reflection
    Exercise set 6 (Generated/Free/Initial and institutions)
41. Foundations 7: data structures (data invariants, congruence relations, arrays and tuples); substitutions
    Exercise set 7 (Data structures and algebra constructions)
42. Foundations 8: inlining, generic programming and institutions — and in Magnolia; procedures and functionalisation
    Exercise set 8 (Generics as an institution interface morphism)
43. Domain engineering the Magnolia way; — API, microservices, software product lines;
    Presentation of compulsory assignment problems (team work)
    Exercise set 9 (Compulsory assignment)
44. Exercise set 9 (compulsory assignment)
45. Exercise set 9 (compulsory assignment)
46. Exercise set 9 (compulsory assignment)
47. Curriculum summary, Q&A
    Voluntary student presentations (Thursday, room Kremle, at 1415): solutions to the compulsory assignments

Exam

The course will be evaluated by an oral exam Monday 27 and Tuesday 28 November 2023.