Last modified: 20070528:101602/update timetable (Tutorials)

CSE4213 AJH-2007-00

CSE4213 Home Page

CSE4213 Formal Methods in Software Engineering Home Page

Quick Links | News | Contact Details | Learning Resources | Problems

Quick Links

HelpDesk Bookings
Anonymous Feedback Page


If anyone has submitted work for assignments 1 and 2 that do not appear to have been marked yet, would they please contact me? I have a number of assignments that have been submitted (either by email or memory stick) that have no identifying data on them, and I am unable to mark them (or at least attribute the marks to the correct person).

Following successful negotiations with the Melbourne Racing Club, Exams Branch is pleased to advise that all students who currently hold a Monash parking permit will be exempt from paying a $6 parking fee at the Caulfield Racecourse during the Semester One 2007 examination period.

The racecourse is well served by train, bus and tram services, and students are encouraged to consider the advantages of travel to their examinations via public transport. However, the following car parking arrangements will apply during the examination period:

Should you have any queries regarding this message, please go to the on-line self help system or phone +61 3 99026011.

Exams Branch


I have been asked to pass on a reminder to students in this unit that mobile phones are not permitted in examinations. The message is:

Important Reminder

No mobile phones allowed in exam

Possession of unauthorised materials in an exam is a discipline offence under Monash Statute 4.1.
Possession includes any items in your pockets, clothing, or on your desk or chair.
Mobile phones are to switched off and placed in your bag or on the floor.

Previous News Items

Contact Details

Lecturer and Unit Coordinator

A/Prof John Hurst. You can call me "John" or "Prof Hurst" as you like, but "Mr Hurst" is deprecated .
Room 123 in Building 63, Clayton campus (Tuesdays and Thursdays).
Room 110 in Building 3b, Clayton campus (Mondays and Wednesdays).
Room 7.78 in Building H, Caulfield campus (Fridays).
(but it is always best if you ring first to check - Presidential duties mean that I am often somewhere else!)
(03) 990 55192
04 0756 9041 (mobile)
John.Hurst at infotech dot monash dot edu dot au (preferred method of contact)
Web Page
John Hurst's Home Page. Note in particular the link to John Hurst's Appointments Schedule, which is useful if you want to know when I am likely to be in my office. You can also make appointments to see me from this page. Note that I am usually at Caulfield on Fridays.
Consultation Hours (building 63, room 123)
1100 Tuesdays (preceeding the lecture)
1000 Thursdays
The Tuesday and Thursday times are "hard coded" into my timetable. However, I run an "open door policy", meaning that if my office door is open, you are free to approach me with any problem you might have. At other times, feel free to make an appointment through my Appointments Page. Note that my office location can vary at short notice from the times posted in Location above.

Tutors and Demonstrators

John Hurst. See under lecturer for details.

See separate page for contact details

Learning Resources

See also the school information page


The lectures will be held at 12noon in R6 on Mondays and 12noon in S1 on Tuesdays.

The lectures are based upon a set of slides kindly supplied by A/Prof Ken Robinson, of the University of New South Wales (my alma mater) and available on-line. The text book, The B-Method, by Steve Schneider, is also used to support the lecture content.

Each lecture has an index page (accessed by clicking the date entries in the following table) which gives links not only to the slides used in lectures, but also to more compact forms, as well as plain paper note form. The latter is the most economical form for printing. Links under "Topics" are to the slides used in lectures.

Please bear in mind that at the time of writing, not all materials to be used in the lectures have been identified. This page will be updated regularly to reflect past practice, current happenings, and future intentions. Lines in red represent completed activities.

Note that the lecture timetable has been restructured so that dates are links to the lecture index page, and the topics are links to the presentation slides.

Lecture Date Topics Covered
01 26 Feb Introduction to B, Brief Introduction to the B-Tool 1-48
02 27 Feb Set Theory, revision of relevant concepts 1-54
  27 Feb Assignment 1 Available
04 6 Mar Abstract Machines, CoffeeClub0, Demonstration of the BToolkit, CoffeeClub1 1-63, 1-38
05 12 Mar CoffeeClub2, Modelling, Taking specification through to implementation , 1-114
06 13 Mar test machine, Formal Definitions of Relations, Functions and Sequences , 1-63
07 19 Mar Library Case Study, a more realistic example 1-98
08 20 Mar Library Case Study (cont), making specifications robust 99-151
09 26 Mar Predicate Logic and Substitutions 1-52
10 27 Mar Discharging Proof Obligations 1-20
11 2 Apr Discharging Proof Obligations 21-30
12 3 Apr Discharging Proof Obligations, Specifying a Simple File System 31-41, 1-38
  4 Apr Assignment 1 Due!
  4 Apr Assignment 2 Available
- 9 Apr Mid-semester break: No lectures this week
- 10 Apr Mid-semester break: No lectures this week
13 16 Apr Specifying a Simple File System 38-54
14 17 Apr (Lecture cancelled due to power outage)
15 23 Apr Specifying a Simple File System , Preconditions and Guards 54-87, 1-60
16 24 Apr Machine Composition 1-27
  27 Apr Assignment 2 Due!
  27 Apr Assignment 3 Available
17 30 Apr Structuring Specifications 1-75
18 1 May Structuring Specifications 76-131
19 7 May Generalised Substitutions 1-30
20 8 May Generalised Substitutions 31-170
21 14 May Traffic Lights, Refinement 1-103, 1-50
23 21 May Beyond Specification 1-36
24 22 May Beyond Specification, Data Design 1-36, 1-21
  23 May Assignment 3 Due!
25 28 May Loop Correctness 1-20
26 29 May revision


Tutorials start in week 1. You will be required to register for a tutorial through Allocate+. The tutorial is scheduled for Mon 1300-1400 in Krongold Centre room KG23. (Lecturer access only: Allocate Admin, TCUP access)

Tutorials will provide an opportunity for more interactive learning than is possible in either lectures or lab sessions. Tutorial questions will be made available through this web page, and you are encouraged to prepare responses to these questions before attending the tutorial session.

An attendance roll will be kept, including details of who participated in discussion. This roll may be used in borderline cases to improve a student's mark (but never downgrade it).

Tute Start Date Tute Sheet Solutions
1 26 Feb Exercise 1, Revision exercises in Sets (1-3) questions 1,2,3
2 6 Mar Tutorial Cancelled
3 12 Mar Exercsie 1, Revision exercises in Sets (4-5) questions 4,5
4 19 Mar Exercsie 1, Revision exercises in Sets (6-8) questions 6,7,8
5 26 Mar Exercise 2, sample specifications (Q1) Simple Bank
6 2 Apr Exercise 2, sample specifications (Q1, robust; Q2)
7 16 Apr Tutorial cancelled due to power outage
8 23 Apr Discussion of Assignment 1; Exercise 2, sample specifications (Q2) Traffic Lights
9 30 Apr Exercises 3
10 7 May The Lift Machine
10 15 May Exercises 4 (array machine)
11 21 May Exercises 4 (snack machine)
12 29 May Exercises 4 (bag machine), revision Bags

Lab Classes

There are no formal lab classes in this unit: however, students are expected to spend a significant amount of time in the sng labs using the B Toolkit.


There are three assignments, each worth 20%, and one 2 hour examination paper, worth 60%.

Please note the assignment submission page at, which details information relating to the submission of assignment work, particularly the requirement that the deadline is 12noon on the date concerned.

Students should consult University materials on cheating, in particular:

  1. Student Resource Guide - section on Student Rights and Responsibilities at
  2. Student Resource Guide at, particularly the section on Cheating at
  3. Faculty policy at
  4. Statute 4.1 on Discipline at
It is the student's responsibility to make themselves familiar with the contents of these documents.

Note that assignments are to be submitted through MUSO. All files associated with the submission should be placed in a tar file, and this tar file should be the sole submission file. The file must be named <your student id>.{} Alternatively, you may submit a single pdf file containing all your work. The file must be named <your student id>.pdf.

Assignment Start Date Due Date Assignment Materials Solutions
1 27 Feb 04 Apr Student Enrolment: Basic Specification
Enrol1 test 1
Enrol1 test 2
test 3
test 4
2 4 Apr 27 Apr Student Enrolment: Courses marking scheme
3 27 Apr 23 May Enrolment System: Design and Learning Outcomes marking scheme


At this stage, there is no FAQ


The course follows the text (as time permits):

Schneider, S.,
The B-Method: An Introduction,
first edition, Palgrave, 2001.
Why is this picture such an interesting pun? The name has one obvious connection. What is the other? What is so interesting about the date? And where was the picture taken?
A bonus mark for the first correct answer to each question.
Discussion on the Anonymous Feedback Page please!

There are two copies of this text in the Hargrave on overnight loan. You may also find Wordsworth's earlier book Software Development with B useful. There are 2 copies of this book in the Hargrave, one on overnight, the others on weekly loan.

Reference Documents

Document Number Document Title and Link Document Number Document Title and Link
2007-00 Home Page (this page) 2007-01 About This Unit
2007-02 Assessment Details 2007-03 Examination Details
2007-04 Resource Details 2007-05 Lecture Details
2007-06 Assignment 1 2007-07 Concise Summary of B Toolkit
2007-08 Tutorial Details 2007-09 Exercises 1
2007-10 Lecture 01 2007-11 Lecture 02
2007-12 Lecture 03 2007-13 Lecture 04
2007-14 Lecture 05 2007-15 Lecture 06
2007-16 Lecture 07 2007-17 Lecture 08
2007-18 Lecture 09 2007-19 Lecture 10
2007-20 Lecture 11 2007-21 Lecture 12
2007-22 Assignment 2 2007-23 Lecture 13
2007-24 Lecture 14 2007-25 Lecture 15
2007-26 Lecture 16 2007-27 Lecture 17
2007-28 Lecture 18 2007-29 Lecture 19
2007-30 Assignment 3 2007-31 Lecture 20
2007-32 Lecture 21 2007-33 Lecture 22
2007-34 Lecture 23 2007-35 Lecture 24
2007-36 Lecture 25 2007-37 Lecture 26

Other Links

  1. Why Design Software?
  2. some helpful set theory pages
  3. Can Software Kill You?

Useful URLs for this unit will be added here.

If you find a useful URL, please send it to John Hurst, so that others can check it out as well.


Got any problems? You can post questions, comments, feedback to the CSE4213 Anonymous Feedback Page. You can use the page anonymously, but it is preferred (and your comments carry more weight) if you use your name or nickname on them.

Document History

20070507:093635 6.0.9 ajh new notices about power outage and lecture rearrangement
20070426:192916 6.0.8 ajh new notices about email and assignments
20070404:083846 6.0.7 ajh add notice about moving offices, and assignment 2
20070327:163440 6.0.6 ajh link to resources page in notices
20070321:111536 6.0.5 ajh notice re absence on 22 Mar
20070306:144918 6.0.4 ajh updated news items
20070306:092732 6.0.3 ajh added quick link to HelpDesk
20070227:155208 6.0.2 ajh add docs 10,11,12,13 (lecture pages), and note about cancelled tutorial.
20070226:100928 6.0.2 ajh add docs 07,08,09
20070220:121558 6.0.1 ajh add doc 06, assignment 1
20070130:165501 6.0.0 ajh initial page for 2007

Document History (Lecturer_Details)

20070523:143933 6.0.2 ajh fixed appointments page link
20070404:083651 6.0.1 ajh updated building and room details
20070202:185439 6.0.0 ajh initial version for 2007

Document History (Tutorials)

20070528:101602 6.0.6 ajh update timetable
20070508:160937 6.0.5 ajh fix multiple timetables and links to exercise directories
20070328:104832 6.0.4 ajh move tutorial exercises to sub-directories
20070326:115218 6.0.3 ajh update tutorial details for Exercises 2
20070314:160214 6.0.2 ajh update tutorial details
20070226:101217 6.0.1 ajh add tutorial time and room details
20070220:122300 6.0.0 ajh initial version for 2007

Document History (Assessment_Discussion)

20070507:094357 6.0.2 ajh add detail about assignment submission
20070403:104202 6.0.1 ajh add instruction about submission
20070206:143936 6.0.0 ajh initial version for 2007

Document History (Assessment_Schedule)

20070507:095004 6.0.2 ajh added detail about assignments 2 and 3
20070220:121805 6.0.1 ajh added assignment 1
20070206:144217 6.0.0 ajh initial version for 2007

This page maintained by John Hurst.
Copyright Monash University Copyright Policy
4524 accesses since
26 Feb 2007
My PhotoTrain Photo

Generated at 20130519:0013 from an XML file modified on 20070601:1125
Maintainer use only; not generally accessible: Local Server Work Server CSSE Server

5042 accesses since 26 Feb 2007, HTML cache rendered at 20140423:2303