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 |
14 Jul |
01 |
|
|
1,2,4
|
Introduction to this Unit,
Introduction to B
|
1-2 |
1-25 |
| 1 |
14 Jul |
|
01 |
|
|
Set Theory Revision (Q1)
|
pdf version |
| 1 |
16 Jul |
02 |
|
|
1,2,4
|
Introduction to B
,
Revision of Set Theory
|
2-4, 1-2
|
26-50, 1-22
|
| 2 |
21 Jul |
|
|
|
|
handout:
Assignment 1
|
|
| 2 |
21 Jul |
03 |
|
|
1 |
Revision of Set Theory,
Abstract Machines
|
1-2 |
23-54, 1-8
|
| 2 |
21 Jul |
|
02 |
|
1 |
Set Theory Revision (Q2-Q4) |
pdf version |
| 2 |
23 Jul |
04 |
|
|
|
Abstract Machines, Abrial's Introduction to Event-B
|
NA |
9-63, 1-13
|
| 2 |
23 Jul |
|
|
|
|
handout:
Discussion 1
|
pdf version |
| 3 |
28 Jul |
05 |
|
|
|
Abrial's Introduction to Event-B |
NA |
14-34 |
| 3 |
28 Jul |
|
03 |
|
|
Set Theory Revision (Q4-Q6) |
pdf version |
| 3 |
30 Jul |
06 |
|
|
|
Formal Definitions of Relations, Functions and Sequences
|
1-13 |
1-63 |
| 4 |
04 Aug |
07 |
|
|
|
Birthday Book tutorial (Using Rodin), Library Case Study
|
NA |
2-4, 1-20
|
| 4 |
04 Aug |
|
04 |
|
|
Set Theory Revision (Q6-Q8) |
pdf version |
| 4 |
06 Aug |
08 |
|
|
1 |
Abrial's Mathematical Background
|
NA |
1-68 |
| 4 |
06 Aug |
|
|
|
|
close: Discussion 1 |
|
| 5 |
11 Aug |
09 |
|
|
1,2,4,10
|
Abrial's Mathematical Background
|
NA |
69-133 |
| 5 |
11 Aug |
|
05 |
|
|
Simple Event-B Machines |
pdf version |
| 5 |
13 Aug |
10 |
|
|
12,13
|
The Square Root Machine
|
1-9 |
1-28 |
| 5 |
13 Aug |
|
|
|
|
return: Discussion 1 |
|
| 5 |
13 Aug |
|
|
|
|
due:
Assignment 1
|
|
| 5 |
13 Aug |
|
|
|
|
handout:
Discussion 2
|
pdf version |
| 6 |
18 Aug |
11 |
|
|
|
Preconditions and Guards,
Substitutions
|
|
1-60, 1-62
|
| 6 |
18 Aug |
|
06 |
|
|
Simple Event-B Machines |
pdf version |
| 6 |
20 Aug |
12 |
|
|
|
Generalized Substitutions |
1-11 |
1-117 |
| 6 |
20 Aug |
|
|
|
|
handout:
Assignment 2
|
|
| 7 |
25 Aug |
13 |
|
|
|
Semantics and Proof Obligations in Event-B |
1-8 |
1-82 |
| 7 |
25 Aug |
|
07 |
|
|
The Lift Machine |
pdf version |
| 7 |
27 Aug |
14 |
|
|
13 |
The Bridge Problem
|
1-12 |
1-12 |
| 7 |
27 Aug |
|
|
|
|
close: Discussion 2 |
|
| 8 |
01 Sep |
|
|
|
|
return: Assignment 1 solutions
|
|
| 8 |
01 Sep |
15 |
|
|
|
(Lecture Cancelled) |
|
|
| 8 |
01 Sep |
|
08 |
|
|
(Tutorial Cancelled) |
|
| 8 |
03 Sep |
16 |
|
|
|
(Lecture Cancelled) |
|
|
| 8 |
03 Sep |
|
|
|
|
handout:
Discussion 3
|
pdf version |
| 9 |
08 Sep |
17 |
|
|
|
(Lecture Cancelled) |
|
|
| 9 |
08 Sep |
|
09 |
|
|
(Tutorial Cancelled) |
|
| 9 |
10 Sep |
18 |
|
|
|
Discussion of
Assignment 1,
CURRENCY and
PURSE components.
|
|
|
| 10 |
15 Sep |
19 |
|
|
|
Abrial Proof Obligations
|
|
1-61 |
| 10 |
15 Sep |
|
10 |
|
|
The Bag Machine
|
|
| 10 |
17 Sep |
20 |
|
|
|
The File Protocol
|
|
1-62 |
| 11 |
22 Sep |
21 |
|
|
|
The File Protocol
|
|
63-121 |
| 11 |
22 Sep |
|
11 |
|
|
Refinement |
pdf version |
| 11 |
24 Sep |
22 |
|
|
|
Refinement Revisited |
|
1-89 |
| 11 |
24 Sep |
|
|
|
|
handout:
Discussion 4
|
pdf version |
| 11 |
24 Sep |
|
|
|
|
return: Discussion 2 |
|
| 11 |
24 Sep |
|
|
|
|
due: Assignment 2 |
|
| 11 |
26 Sep |
|
|
|
|
close: Discussion 3 |
|
| |
29 Sep |
- |
|
|
|
Mid-semester (!) break - no lectures this week
|
|
|
| |
01 Oct |
- |
|
|
|
Mid-semester (!) break - no lectures this week
|
|
|
| |
03 Oct |
|
|
|
|
return: Discussion 3 |
|
| 12 |
06 Oct |
23 |
|
|
|
Refinement Revisited |
|
90-151 |
| 12 |
06 Oct |
|
12 |
|
|
Refinement (Traffic Lights again) |
pdf version |
| 12 |
08 Oct |
24 |
|
|
|
Refinement Revisited
lectopia recording
|
|
152-245 |
| 12 |
08 Oct |
|
|
|
|
close: Discussion 4 |
|
| 12 |
08 Oct |
|
|
|
|
return: Assignment 2 |
|
| 13 |
13 Oct |
25 |
|
|
|
revision |
|
|
| 13 |
15 Oct |
26 |
|
|
|
revision
Lectopia recording of revision discussion
|
|
|
| 13 |
15 Oct |
|
|
|
|
return: Discussion 4 |
|
