The Magic of Specifications and Type Systems

by on 17 June and 15 August 2017
plain text via web or gopher [?]

I took the Computer Science Project course, EECS 4080, in summer 2016. My main objective was learning Haskell and to gain some experience with working on formal methods.

I had the privilege of working with Prof. Jonathan Ostroff and Simon Hudon, mainly on two projects:

  1. Literate Unit-B, the verifier for the Unit-B formal method, and
  2. Unit-B Web, a web interface using Literate Unit-B for doing predicate calculus proofs.

From the Literate Unit-B codebase, written in Haskell, I decoupled the logic module and used it to build Unit-B Web, also written in Haskell, which supports the LaTeX syntax of the Unit-B logic, renders user input on the page, and calls the sequent prover of the logic module, which uses the Z3 SMT solver to check the validity of user input.

Further, I did a major refactoring that separated the type checker of Literate Unit-B from its parser. Among other things, this refactoring paves the way for my next task of implementing subtyping, as volunteer work.

In addition to presenting my work for the final presentation of EECS 4080 on 18 August 2016, I also presented it on 17 June 2017 at the Canadian Undergraduate Computer Science Conference 2017 held at the University of Toronto, and on 15 August 2017 at the Lassonde Undergraduate Summer Student Research Conference held at York University.

Abstract

Writing specifications for complex software is as important as blueprints are for skyscrapers and bridges that are safe and fit for their purpose. The aim of this project is to take a step towards making writing specifications for software more readily and more easily accessible, and taking advantage of the power of type systems along the way.

For this, I built Unit-B[*] Web, a web interface for doing predicate calculus proofs. Ultimately, Unit-B Web leverages the power of the Z3 verifier to two purposes:

  1. Teaching: Unit-B Web can be used in the classroom for demonstrations, or in evaluation in the form of online quizzes; and
  2. online proof environment: making tooling for set theory, functions, relations, arithmetic, intervals, and predicate calculus theories available on the web, Unit-B Web serves as a proof of concept for a web IDE for the full modeling capabilities of Unit-B.

Logic is fulfilling more and more the promise of aiding computer scientists and software engineers develop more reliable software, by enabling them to work at a more abstract level to write more concise specifications. The goal of Unit-B Web is to help by making specifications more accessible to casual users.


[*] Unit-B is a new framework for specifying and modeling systems that must satisfy both safety and liveness properties.

The presentation poster and slides (and their sources) are available:

[poster for Magic of Specifications and Type Systems]
‘Magic of Specifications and Type Systems’ poster
[slides for Magic of Specifications and Type Systems]
‘Magic of Specifications and Type Systems’ slides