INF220 - Programvarespesifikasjon
Autumn 2021
Contents on this web page
The course is about the design and reuse of software components.
For this we use the framework of institutioni theory and algebraic specifications.
The theory is illustrated with practical programming in Magnolia.
Magnolia is an experimental programming language tightly integrating specifications and code.
Its semantical model can map directly to hardware, allowing usi, e.g., to program GPUs.
Compiled code can be run as command line applications or microservices.
The language design 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 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.
- 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).
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) and text book.
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.
Lecturer and course responsible: Magne Haveraaen
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.
Please also keep me informed if you cannot make it to a lecture.
I will try to stream the lectures for those who are in quarantine. See MittUiB for details.
See the official schedule, subject to change:
- Tuesdays 1415 - 1600 in seminar room 302O1 HiB
- Wednesdays 1015 - 1200 in seminar room 302O1 HiB
- Fridays 0815 - 1000 in seminar room 302O1 HiB
Teaching starts Tuesday 24 August 2021 (week 34),
Teaching will be in the form of lectures, exercises and
time off for self studies.
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).
The following teaching plan is very tentative and guaranteed to change.
- 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
The exam is planned for the end of November/beginning of December.
The exercises will be provided as the course evolves,
check mittuib.
The course will be evaluated by an oral exam.
Last updated 2021-08-20 by
Magne Haveraaen