Skip to content | Change text size
Handbooks Courses Units Related information

FIT3013 - Formal specification for software engineering

6 points, SCA Band 2, 0.125 EFTSL

Undergraduate Faculty of Information Technology

Leader(s): John Hurst


Clayton First semester 2009 (Day)


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 Event-B notation, data and algorithm design; data and operation refinement; proofs of correctness; proof obligations.


  1. Fundamentals of the B Method;
  2. Applications of the B Method;
  3. A reading knowledge of B specifications;
  4. Software Testing in the discrete domain;
  5. The role of proof obligations and consistent specifications;
  6. Determination of Proof Obligation;
  7. The role of refinement in developing formal specifications;
  8. An appreciation of the professional need to establish formal properties of software;
  9. A belief that formal specifications can improve the quality of software;
  10. Skills in using the B notation to develop and prove software specifications;
  11. The ability to install a B Toolkit on a Unix/Linux platform;
  12. The ability to write basic B specifications;
  13. The ability to refine and extend more advanced B specifications.


Assignments: 50%
Examination: 50%

Contact hours

3 x contact hrs/week


FIT2004 and (MAT1830 or MTH1112 or MAT1077)


CSE4213, GCO4013, SFT3302

Additional information on this unit is available from the faculty at:

[an error occurred while processing this directive]