In this table, green entries have been released to students,
black entries are in draft form or not yet available,
while red entries indicate activities that have been completed.
| Week |
Date |
Lecture |
Tute |
Lab |
Objs |
Content |
Notes |
PDFs |
| 1 |
03 Mar |
01 |
|
|
1,2,4
|
Introduction to this Unit,
Introduction to Event B
|
1-2 |
1-50 |
| 1 |
03 Mar |
|
|
|
1,3,8,10,12
|
handout:
Assignment 1a
|
pdf version |
| 1 |
04 Mar |
02 |
|
|
1 |
Abrial's Introduction to Event-B |
NA |
1-30 |
| 1 |
04 Mar |
|
|
|
1,3,11
|
handout:
Discussion 1
|
pdf version |
| 2 |
10 Mar |
|
01 |
|
11 |
Use of Rodin |
|
| 2 |
10 Mar |
03 |
|
|
1 |
Abrial's Introduction to Event-B,
Revision of Set Theory
|
NA, 1-3
|
27-34, 1-58
|
| 2 |
11 Mar |
04 |
|
|
1 |
Use of Rodin,
The Parking Meter Example
,
Abrial's Mathematical Background
|
NA |
1-33 |
| 3 |
17 Mar |
|
02 |
|
1 |
Set Theory Revision (Q1-Q3)
|
pdf version |
| 3 |
17 Mar |
05 |
|
|
1 |
Abrial's Mathematical Background
|
NA |
34-90 |
| 3 |
18 Mar |
06 |
|
|
1 |
Abrial's Mathematical Background
|
NA |
90- |
| 4 |
24 Mar |
|
03 |
|
1 |
Set Theory Revision (Q4), Set Theory Revision (Q5-Q6)
|
pdf version, pdf version
|
| 4 |
24 Mar |
|
|
|
|
due:
Assignment 1a
|
|
| 4 |
24 Mar |
07 |
|
|
3,10,12
|
Abstract Machines
,
The Bridge Problem
|
1-9, 9-16
|
1-61, NA
|
| 4 |
25 Mar |
08 |
|
|
1,2,3,12,13
|
The Bridge Problem
|
9-16 |
NA |
| 4 |
25 Mar |
|
|
|
|
close: Discussion 1 |
|
| 4 |
25 Mar |
|
|
|
1,3,8,10,12
|
handout:
Assignment 1b
|
pdf version |
| 5 |
30 Mar |
|
04 |
|
|
Rodin and Refinement |
pdf version |
| 5 |
30 Mar |
09 |
|
|
|
Simple Library Machine
|
|
1-79 |
| 5 |
01 Apr |
|
|
|
|
return: Discussion 1 |
|
| 5 |
01 Apr |
10 |
|
|
|
Bridge Demo |
|
|
| |
07 Apr |
- |
|
|
|
Mid-semester (!) break - no lectures this week
|
|
|
| |
08 Apr |
- |
|
|
|
Mid-semester (!) break - no lectures this week
|
|
|
| 6 |
14 Apr |
|
|
|
|
due:
Assignment 1b
|
|
| 6 |
14 Apr |
|
05 |
|
|
Simple Library Machine Development, Simple Event-B Machines: Bank
|
pdf version, pdf version
|
| 6 |
14 Apr |
11 |
|
|
|
Semantics and Proof Obligations in Event-B |
1-8 |
1-86 |
| 6 |
15 Apr |
12 |
|
|
|
Abrial Proof Obligations
|
|
1-41 |
| 7 |
21 Apr |
|
06 |
|
|
Simple Event-B Machines: Traffic Lights |
pdf version |
| 7 |
21 Apr |
13 |
|
|
|
Abrial Proof Obligations
|
|
42-60 |
| 7 |
22 Apr |
14 |
|
|
7,10,12,13
|
The Square Root Machine
|
1-12 |
1-78 |
| 8 |
27 Apr |
|
|
|
1,2,4,9
|
handout:
Discussion 2
|
pdf version |
| 8 |
28 Apr |
|
07 |
|
|
Simple Event-B Machines: Lift Machine |
pdf version |
| 8 |
28 Apr |
15 |
|
|
|
Sorting Algorithms
,
Sorting Algorithms
|
|
1-51, 52-62
|
| 8 |
29 Apr |
16 |
|
|
|
Sorting Algorithm Example
,
Sorting Algorithms (revised)
|
|
1-49, 1-81
|
| 8 |
29 Apr |
|
|
|
|
return:
Assignment 1 solutions
|
pdf version |
| 8 |
29 Apr |
|
|
|
|
handout:
Assignment 2
|
|
| 9 |
05 May |
|
08 |
|
|
The Supermarket
|
pdf version |
| 9 |
05 May |
17 |
|
|
|
Preconditions and Guards,
Logic and Substitutions
|
1-11, 1-11
|
1-61, 1-61
|
| 9 |
06 May |
18 |
|
|
|
Substitutions |
1-11 |
1-61 |
| 10 |
12 May |
|
09 |
|
|
More Refinement Examples |
pdf version |
| 10 |
12 May |
19 |
|
|
|
The File Transmission Protocol
|
|
1-61 |
| 10 |
13 May |
20 |
|
|
|
The File Transmission Protocol
|
|
62-121 |
| 11 |
19 May |
|
10 |
|
|
CANCELLED |
|
| 11 |
19 May |
21 |
|
|
|
CANCELLED |
|
|
| 11 |
20 May |
22 |
|
|
|
Refinement Revisited |
|
74-116 |
| 11 |
21 May |
|
|
|
|
close: Discussion 2 |
|
| 12 |
26 May |
|
|
|
|
due: Assignment 2 |
|
| 12 |
26 May |
|
11 |
|
|
Refinement (Traffic Lights again) |
pdf version |
| 12 |
26 May |
23 |
|
|
|
Refinement Revisited |
|
117-237 |
| 12 |
27 May |
24 |
|
|
|
Refinement Revisited |
|
117-237 |
| 13 |
01 Jun |
|
|
|
|
return: Discussion 2 |
|
| 13 |
01 Jun |
|
12 |
|
|
Review of
2008 Exam Paper
|
|
| 13 |
01 Jun |
25 |
|
|
|
revision |
|
|
| 13 |
03 Jun |
26 |
|
|
|
Review of various exam papers |
|
|
| 13 |
25 May |
|
|
|
|
return: Assignment 2 |
|
