Information Systems by Calculation

Objectives

  • Verify software systems by calculation
  • Adopt “Relational Thinking” as a method supported by model checking using the Alloy tool.
  • Express and reason about the key-value-pair database model in a formal way.
  • Carry out correctness proofs using relational algebra.
  • Perform formal validation of software contracts.

Program

  1. Brief introduction to formal methods and their role in programming.
  2. Role of binary relations in abstract problem modeling. Taxonomy and algebra of binary relations.
  3. The motto “everything is a relation”. Model checking using the Alloy tool.
  4. Use of abstract interpretation in complex problem modeling.
  5. Free theorem calculation of functions with polymorphic types.
  6. Correctness proofs using relational algebra.
  7. Relational formalization of the key-value-pair data model.
  8. Limits of static typing. Formal notion of contract. Weakest precondition calculation.
  9. Hoare logic in relational format.

Bibliography

  • J.N. Oliveira. Program Design by Calculation, 2008. Draft of textbook in preparation, current version: October 2019. Chapters 5 to 7. Available from http://www4.di.uminho.pt/~jno/ps/pdbc.pdf. Informatics Department, University of Minho.
  • D. Jackson. Software abstractions: logic, language, and analysis. Revised edition, MIT Press, 2012.
  • C.B. Jones. Systematic Software Development Using VDM. Series in Computer Science. Prentice-Hall International, 1986.

Updated: