This unit is being phased out

Amend synopsis, assessment and prerequisites to match FIT3013 as these units will be co-taught in 2008.

The unit is a relabelling of GCO4013, which was in turn developed from CSC3080. Both of these are now obsolete. All of these units address the problem of defining the formal mathematical behaviour of programs, the first two using the Z specification language, this current one using the B specification language and toolkit.

Review of set theory, the predicate calculus, relations, relational algebra and formal specification concepts; algebraic and model based specifications; the role of formal specifications in software engineering. The B notation, data and algorithm design; data and operation refinement; proofs of correctness; proof obligations.

PRESCRIBED TEXT:

Steve Schneider, The B-Method: An Introduction, Palgrave, Cornerstones of Computing series, October 2001. ISBN 0-333-79284-X.

Assignments: 50% + Examination: 50%

There are three assignments, worth 10%, 20% and 20%, and one 2 hour examination paper, worth 50%.

A tutorial room equipped with data projector (which can be connected to a VGA or DVI laptop) and rj45 network connector (network access) is required. Internet connectivity to a roaming laptop is essential.

Sufficient Unix/Linux machines for 50 students to access the BToolkit. The system is available for students to load onto their own Linux systems (and run under licence).

• Software Title: B Toolkit
• Vendor: B Core Pty Ltd
• Version: 5.1.12
• OS: SNG. Possibly can be made to run under LINUX, but this is untested.
• License Details: 50 seat Site Licence (spelt with two 'C's, notice! 'c' for the noun, 's' for the verb) THIS WILL NEED TO BE RENEWED JUST BEFORE SEMESTER STARTS!
• Are we currently licensed: Yes
• If (Yes), who is the contact person for this software?: Heinx Schmidt/John Hurst
• If (No), will the software license be arranged by: Staff member requesting the software ( ) or Technical Services* ( ) ? *If the latter is selected, please discuss your requirement/s with myself ASAP, prior to finalising your request, as there could be financial or resourcing implications.
• Is the software to be installed and accessed from a: Server
• Type of license: Site Licence and Lab based # of Licenses needed __50__
• In what week will you commence using the software in class? Semester 1 (Week 1 )
• Nominated Staff For Acceptance Testing Software: John Hurst, 55192, ajh@csse.monash.edu.au
• Additional Information: Special Requirements, Software Configuration/Installation Requirements, etc: Needs LaTeX, editor (emacs or vi) and HTML browser (any)

This software is currently installed on SNG and CSSE Solaris machines, version 5.1.4 and 5.1.12 respectively.

The School has a licence for up to 50 concurrent users, and the licence server currently is running on nexus.csse.monash.edu.au (which as a result, cannot itself be used to run the BToolkit).

In 2003, problems were experienced with the number of licences, and the stability of the system under load. In 2004, the number of licences was increased (from 20 to 50), and this problem did not appear. The system was adequately stable in 2005/6

LaTeX is also required on the same machines in order to typeset machine specifications. This is available under the GNU Open Source agreement. B-Toolkit Release 5.1.12_j1.2 Copyright(c) 1985-2002 B-Core(UK) Ltd

NOTE ALSO THAT THERE HAVE BEEN PROBLEMS PRINTING FROM THE SNG MACHINES. It would be appreciated by the students if they did not have to export pdf files from the SNG machines to other machines in order to print them (as required for assignment submission).

(CSE2201 or FIT2024) and (MAT1830 or MTH1112 or MAT1077)