CSE4213 AJH-2003-00 CSE4213 Formal Methods in Software Engineering Home Page


Welcome to CSE4213! This home page should be your first port of call for any information specific to this subject. If the information you seek is not here, drop me a note and I'll endeavour to fix it for you.

This subject has a Handbook Entry on the web. It also has an Anonymous Feedback Page.


The data correctness slides are now available. The latter are also available in condensed lecture note form.
The slides from Prof Schmidt's lecture and the loop correctness slides are now available. The latter are also available in condensed lecture note form.
There are sample exam papers available under the Assessment Page
Due to the problems with everyone trying to access the BKit at once, an extension of time to submit Assignment 2 is granted until 12noon on Thursday 15 May 2003.

CORRECTION! The animation scripts with embedded minus signs in their names don't work. Use these ones instead. Ass2-Test-1 Ass2-Test-2 Ass2-Test-3 Ass2-Test-4

The easiest way to incorporate these into your system is

  1. click the animate button
  2. select "Edit ANIMATE Script", click OK
  3. select "New ANIMATE script", click OK
  4. select "Empty ANIMATE script", click OK
  5. enter a name, click OK
  6. when the editor displays the template, edit the operations to include those in the given (downloaded) script, renaming as appropriate.
  7. save and "Execute Auto" to run the script
  8. Don't forget to save and print the output and include it with your submission.

The animation scripts are now available at (links deleted)
Assignment 2 is now available. The due date is 14 May.

Previous News Items

Contact Details

Learning Resources

Lecture Timetable


Lab Classes


Please note the assignment submission page at http://www.csse.monash.edu.au/subjects/assign_submit.html , which details information relating to the submission of assignment work, particularly the requirement that the deadline is 12noon on the date concerned.

1 12 Mar 19 Mar assessment/Ass1-23.pdf Various pencil and paper exercises

Students should consult University materials on cheating, in particular:

  1. Student Resource Guide - section on Student Rights and Responsibilities at http://www.monash.edu.au/pubs/handbooks/srg/srg0059.htm
  2. Student Resource Guide at http://www.monash.edu.au/pubs/handbooks/srg/, particularly the section on Cheating at http://www.monash.edu.au/pubs/handbooks/srg/srg0071.htm
  3. Faculty policy at http://www.csse.monash.edu.au/~ajh/adt/policies/cheating.html
  4. Statute 4.1 on Discipline at http://www.monash.edu.au/pubs/calendar/statutes/statutes04.html
It is the student's responsibility to make themselves familiar with the contents of these documents.


At this stage, there is no FAQ


The course follows the text (as time permits):

J.B.Wordsworth, Software Engineering with B, first edition, Addison-Wesley, 1996.

There are two copies of this text in the Hargrave on overnight loan. You may also find Wordsworth's earlier book Software Development with Z useful, as it covers the same examples, but using the earlier (but related) specification notation Z. There are 4 copies of this book in the Hargrave, one on overnight, the others on weekly loan.

Reference Documents

Document Number Document Title and Link
00 Home Page (this page)
01 Contact Details
02 About This Unit
03 Timetables
04 Exercises 1
05 Concise Summary of B Toolkit (no on-line version available)
06 Assessment Logistics
07 Labs Description
08 Exercises 2
09 Tutorials
10 Assignment 2

Other Links

As software bugs multiply, questions arise


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

20030527:110419 1.4 ajh News item about sample exam papers
20030513:083846 1.3 ajh News items about animation
20030429:075552 1.2.1 ajh added link to risks story
20030408:091507 1.2 ajh updated msgs
20030303:144239 1.1 ajh added document list
20030122:120848 1.0 ajh Initial Version, developed from 2002 CSE4213 Home Page
This page is copyright, and maintained by John Hurst. 0 accesses since
21 Apr 2019
My PhotoMy PhotoTrain Photo

Local servers: Localhost Newport Burnley Everton Hamilton Bittern Spencer (Note that these are only accessible on my local network.)
Public Web Servers: Hurst Server/ajhurst.org Home Server/ajh.co Internode Server (In order of preference; not all of these may be active.)
Dynamically generated at 20190421:0848 from an XML file modified on 20030616:2223.

112 accesses since 19 Jan 2019, HTML cache rendered at 20190423:0130