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 30% labs and 70% the exam.
The mock exam from 201314 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.
A mock exam from 201415 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.
You can also take a look at last year’s exam paper.

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).
- This Z LaTeX cheatsheet.

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.

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.

On applications and social context

- A paper on language ambiguities by Kamsties, Berry, and Paech. Thanks to Hind Zantout. The paper is on CiteSeer and if you are interested, Daniel Berry’s webpage is a hoot.
John Harrison’s slides on verifying floating-point algorithms.
- 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).

Lectures

Lecture of Monday 12 January at 12:15: Watch it and/or read the slides for lecture 1.
Lecture of Monday 12 January at 15:15: Watch it and/or read the slides for lecture 2.
Lecture of Tuesday 13 January at 16:15: Watch it and/or read the slides for lecture 2.
Lecture of Monday 19 January at 12:15: Watch it and/or read the slides for lecture 3.
Lecture of Monday 19 January at 15:15: Watch it and/or read the slides for lecture 3.
Lecture of Tuesday 20 January at 16:15: Watch it and/or read the slides for lecture 4.
Lecture of Monday 26 January at 12:15: Watch it.
Lecture of Monday 26 January at 15:15: Watch it.
The lecture of Tuesday 27 January at 16:15: was a problem-solving session. We considered relevant parts of the mock exam paper.
Lecture of Monday 2 February at 12:15: Watch it.
Lecture of Monday 2 February at 15:15: Watch it.
Lecture of Tuesday 3 February at 16:15: Watch it.
Lecture of Monday 9 February at 12:15: Watch it.
Lecture of Monday 9 February at 15:15: Watch it.
Lecture of Monday 16 February at 12:15: Watch it.
Lecture of Monday 16 February at 15:15: Watch it.
Lecture of Monday 23 February at 12:15: Watch it.
Lecture of Monday 23 February at 15:15: Watch it.
Lecture of Tuesday 24 February at 16:15: Watch it.
Lecture of Monday 2 March at 12:15: Watch it.
Lecture of Monday 2 March at 15:15: Watch it.
Lecture of Tuesday 3 March at 16:15: Watch it.
Lecture of Monday 16 March at 12:15: Watch it.
Lecture of Monday 16 March at 15:15: Watch it.
Lecture of Tuesday 17 March at 16:15: Watch it.
Lecture of Monday 23 March at 12:15: Watch it.
Lecture of Monday 23 March at 15:15: Watch it.
Lecture of Tuesday 24 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.pdf

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.

Class 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)

Misc