CAS 707, Winter 2019: Assignment 1
prog-prove
document is essentially the
first part of
the Concrete
Semantics book
(PDF),
it is useful to download
the Isabelle
theories
from there, in particular the
demo files for
Part I.
(Many of us have trouble with the Concrete
Semantics home page; I still can reach the inner pages with
he links above directly.)
Assignment Question 1.1 — due Wednesday, Jan. 9, at 10:00 a.m.
Download and install Isabelle2018 from the Isabelle home page and
start familiarising yourself with at least the
jedit
manual
“Isabelle/jEdit”,
and the jedit-manual
available under
“Original jEdit Documentation” in the Documentation panel.
Also start working through the prog-prove
document
“Programming and Proving in Isabelle/HOL”.
In particular, solve at least the exercises 2.1–2.5 at the end of section 2.2,
and strive to also solve exercises 2.6–2.8 at the end of section 2.3.
Make your Isabelle theories literate by using text
comments
to document your work, and also document the problems you are having,
and the problems you have solved with significant effort.
Send your Isabelle theories to the kahl@cas.mcmaster.ca
by
Wednesday, 10 a.m..
Assignment Question 1.2 — due Monday, Jan. 14, 9:00 a.m.
Read the paper “Formally verified software in the real world” and produce a two-page LaTeX document (11pt, with 25mm margins) collecting the main points you gather from this reading, and the main questions and topics that you are not sufficiently familiar with for full understanding.
Submit both LaTeX source and generated PDF. (Submission modality will be announced later.)
Assignment Question 1.3 — due Monday, Jan. 14, 9:00 a.m.
Continue from A1.1 with chapter 2 of the prog-prove
document
“Programming and Proving in Isabelle/HOL”, finishing also the
remaining exercises.
If you had holes in sections 2.2 and/or 2.3, or if you found better
ways to do these, submit your updated solutions, including
documentation of the changes.