The academic aims and overall scope of the module are set out on the CS242 webpage. The module has two main parts, one of which is theoretical and the other practical. Part 1 will introduce the basics of mathematical logic as they apply to specifying and verifying computer systems. This will be taught by Dr Meurig Beynon in weeks 2-4 and weeks 8-10 of Term 2. Part 2 will deal with the practical application of the Alloy tool in supporting specification and verification. It will be taught by Dr Jane Sinclair in weeks 5-7. This website, which is subject to refinement as the module is presented over weeks 2-4, is the definitive guide to how Part 1 of the module will be organised and examined for 2009-10.
The lecture times and venues are Monday 13.00 (F1.07), Tuesday 13.00 (LIB 2), and Friday 9.00 (PS1.28). There will no Friday lectures in Weeks 9 and 10 of Term 2. In place of these two lectures, there will be three lectures in the first week of Term 3. These will be held in CS104 at Monday 13.00, Tuesday 13.00, and Thursday 11.00. Note that the exposition of much relevant material is not well-suited to powerpoint-style presentation or to comprehensive summary in printed handouts. On that basis, you are advised to attend lectures and may be expected to take notes from blackboard/whiteboard presentations as necessary (though the resources available in lecture rooms do not always make this very convenient).
As announced in the lecture 1 and confirmed in lecture 9, there will be a class test covering some of the material in part 1. This will take place in the Monday lecture slot in Week 8 - 1pm in F107 on March 1st. The exercise sheets distributed in weeks 2-4 (see below) cover the syllabus for this class test and may be used in revising for the test. In response to requests for more information about the class test, I have prepared a "trailer" for the class test which shows the overall format of the test and features sample questions numbered 0,1 and 5. The preamble to Question 0 is exactly the same as that in the actual test, and you would be wise to consult it in advance as this may save you valuable comprehension time. Note that the seminars in Week 8 - to be held in F1.11 on Thursday at 11 am and 12 noon as specfied in the schedule below - will be devoted to going over the class test. Due to poor attendance at seminars in week 9, there will be no seminars in week 10.
The slides and notes which make up the lecture material indexed below will be introduced in weeks 2-4 and weeks 8-10 as the module progresses. They are intended to help with studying from the book, and to supply complementary material, not to replace the book. As noted above, not all the material to be presented in lectures can be conveniently recorded in the form of handouts. Note that order in which the lecture material is listed below conforms to that adopted by Huth and Ryan, but does not reflect the order in which the topics will be presented in the lectures. For an indication of the actual lecture content, see the outline lecture record.
Lecture material 1
Fac1 program (an example from H&R)
In weeks 2-4, these seminars will be in S0.13, and for weeks 8-10 they will be in F1.11.
The seminars are intended to help you in tackling the Exercise sheets, which give helpful preparation for the examination.
The tutor for the seminars (weeks 3-4 and 8-10) is Ebrahim Ardeshir, a PhD student. For feedback on your solutions, hand them in to DCS reception staff to pass on to Ebrahim before 5pm on Mondays preceding the seminars. From week 3, Ebrahim will have an office hour at 3pm on Tuesday afternoons when he will be available for consultation regarding the exercise sheets.
Four revision seminars were to be given by Ebrahim in weeks 2-5 in Term 3. These have now been cancelled due to lack of interest. Students with problems should see Ebrahim during his office hour (see above).
There will be a two hour examination in June 2010. The examination contributes 60% to the overall mark for the module. There will be five questions, each worth 25 marks, of which you will be expected to answer four. All the questions will be based on the lecture material presented in the Part 1 of the module. (Note that the applications of Alloy that are introduced in Part 2 of the module will not be represented in the examination.)
The June 2008 CS242 examination paper is a reasonably accurate guide to the style and content of this year's examination paper. You may also wish to consult the following sample paper. You can find some notes by way of partial answers to the questions on the sample paper here.
Here is some feedback on the January 2009 CS242 exam paper.
