I'm teaching the ‘formal specification’ course in January-April 2010. Here are some details you may find useful.
The book
This course is based on Ed Currie's excellent book The Essence of Z (available on campus from Blackwell's).
I recommend this, and I also recommend Jonathan Bowen's book on Z “Formal Specification and Documentation Using Z”.
This is a lot hefter than Currie's book — if you use it you'll have to keep calm and search in it for the answers you need — but it has the advantage of being freely available online.
Both books are very well-written.
Slides and videos for the current year are below.
Both books are very well-written.
Slides and videos for the current year are below.
Asking me questions
I won't generally answer questions e-mailed to me directly because you're all generally having the same difficulties. Use Haggis instead.If you have a truly unique problem ... like ... you visited the wrong kind of club last night and a hand-like alien being with acid blood and a long tail shoved a tube down your throat, and you woke up this morning feeling something moving around in your chest cavity — then you can e-mail me directly.
The times
-
Monday, 12:15, EM336.
- Tuesday, 14:15, EM336.
- Thursday, 12:15, EM183.
- There is also a lab on Monday in EM250 from 15:15 to 17:15.
- Tuesday, 14:15, EM336.
Z fonts
This Z font (.ttf) is compatible with Microsoft Windows and should let you type Z symbols in Word. This Z font is compatible with the Apple Mac (.sea). You might also be interested in CutePDF, a free PDF converter; it installs itself as a printer, which you just select to print to from within any program running under Windows, to produce a .pdf file.Class tests
The first class test took place on Monday Feburary 15th 2010. Here is the original script and here is a version with model answers. The test was substantially based on Exercise 3 (the `bidding system') mentioned below.A pre-valentine's class test took place on Monday 8 February 2010. The test with model answers, is available, and also go to the Haggis thread to see students' answers, marked by me online (good source for typical student errors, with corrections).
Class tests from last year are:
- Number 1.
-
Thanks to John Pirie for model answers. I have checked these. They are nearly perfect, except for three major corrections which I added.
Check it out for two model answers to the Resident Evil exercise.
I include John's mistakes as well as the parts he did perfectly. Check it out for mistakes you're liable to make, and my corrections to them. - Number 2 (mock).
Module descriptor
The CS course handbook has the module descriptor for F29FS on page 64. The coursework is worth 30%, the exam is worth 70%.Slides
If you spot typos contact me. Note: the videos are just avi files (typically 150-300Mb). They are not streaming video. This is because of technical limitations; online streaming video services only allow 10 minutes of video, and I do not want to administer my own streaming video server from the department.Downloading these videos to your Heriot-Watt filespace may fail, if the file exceeds your filespace quotas. In that case, download onto a USB stick or other mass storage device instead.
Supplementary lecture notes from John Harrison and Greg Michaelson are here.
-
Lecture 1, 20100111.
(Introduction; Propositions) -
Lecture 2, 20100112.
(Predicates; Quantifiers; Sets) - Here are some online resources for playing with truth-tables: ttable, a handy perl script for making truth tables. An online truth table generator is here (from a logic course online at the University of Kentucky). Some online exercises. More online exercises and solutions.
-
Lecture 3, 20100114.
(More on sets: subset, cardinality, types) -
Lecture 4, 20100118.
(Schema, specifications) - As part of my continuing commitment to facilitating student learning, here is the missing pair of pages, photographed from my own, older edition of the same book.
(Discussing the first lab session. Lots of predicates.)
Discussion
[video]
[video]
[video]
[video]
[video]
Problem sets
Buy or borrow the book and write them up as questions on Haggis.I have released some exercises: try Exercise 4 and Exercise 3. I won't lie to you; they're a bit stodgy. However, they seem to me to be pretty good practice.
I have released some more exercises: try Exercise 1 and Exercise 2.
Extra-curricular
Not everything is formal spec. Here are a few extra-curricular details I may have mentioned:- Japanese Cinema
- For violent movies, try Sonatine or Boiling Point (which I confused with Hard Boiled, a good John Woo action movie). For a classic epic, try Kagemusha.