Formal Specification (F28FS)
Course overview
Welcome to the Formal Specification webpage. In a nutshell, this course says:
“How do we know programs do what we say they do? Hang on—how do we even say what programs do?”
Assessment
- Assessment will be 40% labs and 60% the exam.
- A mock exam is available, in two versions: the mock exam without solutions and should be done first, then you can look at the mock exam with solutions. Let me know if you spot errors and feel free to ask questions.
- You can also take a look at last year’s exam paper.
- Labs were administered weekly (as F28PL was, last semester).
Exercises …
… are here.
Tutorials and Groupwork
Every week or two I devote a timeslot to groupwork. It makes a very interesting change from lectures and you seem to enjoy it a lot. It’s particularly important that you try to turn up to tutorials, because by their participative nature they cannot be filmed or scripted.
Still; I can write up the questions after.
Z resources
- Michael Butler’s introductory notes on specification with Z.
- Terry Marris’s exercises on Z are excellent drill.
- Spivey’s Z notation reference manual is a great tutorial introduction to Z.
- Jonathan Bowen’s Z book makes pretty good reading (the treatment of Z starts in Chapter 3, but Chapters 1-2 are also interesting for background).
SML resources
- I like this intro to SML.
- The standard SML basis library is useful if you want to explore what built-in functions are available.
On applications and social context
- John Harrison’s slides on verifying floating-point algorithms.
- Clachar and Grant’s study of Formalizing UML Software Models of Safety Critical Systems.
- You might find Ian Sommerville’s Chapter 27 on formal specification interesting reading—especially the first two pages, which it seems to me are a beautiful instance of an author having a really good rant.
- An interesting blog post on QuickCheck, randomised testing (for Haskell).
Typesetting resources
- The Objective Z user guide for typesetting Z in LaTeX.
- A MathJax dynaming rendering page.
- You may find the LaTeX OZ (Object Z) package useful, as well as this list of symbols provided by OZ.
- An online LaTeX equation editor and LaTeX to Unicode converter.
Lectures
- Lecture of Monday 13 January at 12:15
- Watch it and/or read the slides for lecture 1 (lecture 1).
- Lecture of Monday 13 January at 15:15
- Watch it and/or read the slides for lecture 2 (lecture 2).
- Lecture of Tuesday 14 January at 16:15
- Watch it and/or read the slides for lecture 2.
- Lecture of Monday 20 January at 12:15
- Watch it and/or read the slides for lecture 2 and lecture 3.
- Lecture of Monday 20 January at 15:15
- Watch it and/or read the slides for lecture 3.
- Lecture of Tuesday 21 January at 16:15
- This was Tutorial I.
- Lecture of Monday 27 January at 12:15
- Watch it and/or read the slides for lecture 3 and lecture 4.
- Lecture of Monday 27 January at 15:15
- Watch it and/or read the slides for lecture 4.
- Lecture of Tuesday 28 January at 16:15
- Watch it and/or read the slides for lecture 5.
- Lecture of Monday 3 February at 12:15
- Watch it. This was a tutorial in which we discussed how to specify a handheld tally counter in Z.
- Lecture of Monday 3 January at 15:15
- Watch it. We continued the tally counter example. 25 minutes and 46 seconds into the lecture we continued with lecture 5. 32 minutes and 25 seconds into the lecture we continued to lecture 6. 32 minutes and 56 seconds into the lecture we agreed that lecture 6 could be deferred to later, and we continued to lecture 7. Nice to make progress.
- Lecture of Tuesday 4 February at 16:15
- Watch it and/or read the slides for lecture 7.
- Lecture of Tuesday 11 February at 16:15
- Watch it and/or read the slides for lecture 7.
- Lecture of Monday 17 February at 12:15
- Watch it. We considered tutorial II and then made a start on lecture 8 .
- Lecture of Monday 17 February at 15:15
- Watch it and/or read the slides for lecture 8.
- Lecture of Tuesday 18 February at 16:15
- Watch it and/or read the slides for lecture 9.
- Lecture of Tuesday 25 February at 16:15
- This was Tutorial III.
- Lecture of Monday 3 March at 12:15
- Watch it and/or read the slides for lecture 9.
- Lecture of Monday 3 March at 15:15
- Watch it; we covered ML. See also the programming languages course.
- Lecture of Tuesday 4 March at 16:15
- Watch it and/or read the slides for lecture 10.
- Lecture of Monday 10 March at 12:15
- Watch it and/or read the slides for lecture 11.
- Lecture of Monday 10 March at 15:15
- Watch it and/or read the slides for lecture 11.
- Lecture of Tuesday 11 March at 16:15
- Watch it and/or read the slides for lecture 11 and lecture 12.
- Lecture of Monday 17 March at 12:15
- Watch it and/or read the slides for lectures lecture 12 and lecture 13.
- Lecture of Monday 17 March at 15:15
- Watch it and/or read the slides for lecture 14.
- Lecture of Tuesday 18 March at 16:15
- Watch it and/or read the slides for lecture 15.
- Lecture of Monday 24 March at 12:15
- Watch it.
- Lecture of Monday 24 March at 15:15
- Watch it.
- Lecture of Tuesday 25 March at 16:15
- Watch it.
- Lecture of Monday 31 March at 12:15
- Watch it.
- Lecture of Monday 31 March at 15:15
- Watch it.
- Lecture of Tuesday 1 March at 16:15
- Watch it.
Full list of lecture slides
lecture-1.pdf lecture-2.pdf lecture-3.pdf lecture-4.pdf lecture-5.pdf lecture-6.pdf lecture-7.pdf lecture-8.pdf lecture-9.pdf lecture-10.pdf lecture-11.pdf lecture-12.pdf lecture-13.pdf lecture-14.pdf lecture-15.pdfClass times
- Mondays at 12:15 in EM3.36.
- Mondays at 15:15 in DB1.13.
- Tuesdays at 16:15 in EM1.82.
- There is a lab Tuesdays at 17:15 in EM2.50.
The Rules
1. Turn up!
2. Understand lecture materials as you get them.
3. A student who thinks “I don’t understand this now; I’ll sort it out during the holidays” is in denial (look at 1m03s).
4. Rules 1-3 above apply especially to those who believe rules 1-3 above don’t apply to them.
Suggested films
You might like to watch:
- Jumper, for illustrating the importance of the initial state of a system (you don’t want the initial state of your otherwise perfect system be 100 feet up in thin air).
- Warm Bodies, for daring to imagine that Romeo and Juliet can be remade as a Zombie teen romance.
- Finding Nemo (for the sharks scene),
- Despicable Me (for minions).
- Terminator and 12 Monkeys (for logically valid but undesirable attempted implementations of the specification “bring peace to Earth”),
- Star Wars (for Obi-Wan’s comment to Luke about truths depending on one’s point of view),
- Blade Runner (for a personal lecture by Rutger Hauer), and
- RoboCop, for Murphy’s assertion that “\( \text{coming with me}(x,y) \)” is a tautology, where \( x:\mathsf{PERP} \) and \( y:\mathsf{LIFESTATE} \) and \( \mathsf{LIFESTATE} ::= \mathsf{dead} \mid \mathsf{alive} \).
- Scanners, for the totally realistic portrayal of what happens to undergraduate students who think about quantifiers.
Suggested books
- Tyler Hamilton’s The secret race. An insider’s account of the gob-smacking doping-related shenanigans got up to by some professional racing teams.
- Joseph Heller’s Catch 22. A book unlike any other I have read, and again important for quotes and references, such as the expression “Catch 22”.
Or then again, you could just watch Youtube, and then watch more Youtube, then read this, then watch this brilliant clip on Vimeo.
A bit about me
I am a researcher in theoretical computer science. My research is mostly in formal logic.
Everybody calls me Jamie but my name is actually Murdoch. You can contact me by e-mail on “gabbay at macs hw ac don’ttypethis uk”. My office is G.50 Earl Mountbatten Building.
The students
Ah, well. I’m glad you asked. You should be second year undergraduate students. Let me know if this is not the case; I’d be interested to know!
A propos nothing in particular
- Revised log levels proposal: “FYI” “WTF” and “OMG” (John Barnette)