The Magic of Specifications and Type Systems
17 June and 15 August 2017
I took the Computer Science Project course, EECS 4080[1],
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[2]
and Simon Hudon[3], 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[4] and slides[5] and their sources[6] are
available.
[ magic-eecs4080-poster.png[7] ]
Magic of Specifications and Type Systems poster preview
[ magic-eecs4080-slides.png[8] ]
Magic of Specifications and Type Systems slides preview
[1]
https://wiki.eecs.yorku.ca/course_archive/2015-16/S/4080/
[2]
https://www.eecs.yorku.ca/~jonathan/
[3]
https://github.com/cipher1024
[4]
https://kelar.org/~bandali/talks/magic-eecs4080-poster.pdf
gopher://kelar.org/d/~bandali/talks/magic-eecs4080-poster.pdf
[5]
https://kelar.org/~bandali/talks/magic-cucsc-2017-slides.pdf
gopher://kelar.org/d/~bandali/talks/magic-cucsc-2017-slides.pdf
[6]
https://git.gnu.ca/~bandali/cucsc-2017
[7]
https://kelar.org/~bandali/talks/magic-eecs4080-poster.png
gopher://kelar.org/I/~bandali/talks/magic-eecs4080-poster.png
[8]
https://kelar.org/~bandali/talks/magic-cucsc-2017-slides.png
gopher://kelar.org/I/~bandali/talks/magic-cucsc-2017-slides.png
Copyright (c) 2016, 2017 Amin Bandali. This work is licensed
under CC BY-SA 4.0.
