INF220 - Program Specification

INF220 - Programspesifikasjon

Autumn 2019

Contents on this web page

Course outline and curriculum

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.
  1. Algebraic specifications as a means of defining API (application programmer interface) contracts.
  2. Institutions as a means of understanding modularisation, reuse and testing.
  3. Generic programming for reuse and correctness testing.
  4. Data invariants and congruences as a means for data abstraction and verification.
  5. Assertions as a means of understanding algorithms.
  6. Pre-/post-conditions as a means of understanding methods.

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

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

Additional Reading Material

For those especially interested in reading up on the background material, the following (classical) books are recommended.

Teachers

Lecturer and course responsible: Magne Haveraaen
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.

Schedule for lectures and seminar groups

See the official schedule, subject to change: Teaching starts Monday 19 August 2019 (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).

Semester plan

The following teaching plan is very tentative and guaranteed to change.
  1. Introduction
    Magnolia overview (language and library), algebraic specifications: interface, algebra (theory)
    Algebraic specifications: expressions, evaluation (theory)
  2. Exercise set 1 (Set theory)
    Exercise set 2 (Installing Magnolia)
    Algebraic specifications: specification logics (theory)
  3. Algebraic specifications: module reuse (theory, Magnolia)
    Magnolia specifications: semigroup, monoid, group.
    Exercise set 3 (Magnolia tutorial)
  4. Algebraic specifications (expressiveness): API vs logic (theory)
    Magnolia specifications: preorders, lattices, sheaves.
    Exercise set 4
  5. Algebraic specifications: institutions (theory, Magnolia)
    Presentation of a practical problem to be solved using Magnolia
  6. Hackathon/Exercise set 5 (2 full days): solving the problem in Magnolia
  7. Student presentations: solution to the problem (compulsory)
  8. Tuples, data invariants and congruences
  9. TBD
  10. TBD
  11. Assertions, pre-/post conditions
  12. Software development
  13. TBD
  14. Data abstraction
The exam is planned for the end of November/beginning of December.

Exercises

The exercises will be provided as the course evolves, check mittuib.

Exam

The course will be evaluated by an oral exam.
Last updated 2019-08-19 by Magne Haveraaen