CAS 707, Winter 2019: Assignment 1

2019-01-10 Update: Since the 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.