UQ Students should read the Disclaimer & Warning

Note: This page dates from 2005, and is kept for historical purposes.

The University of Queensland
School of Information Technology and Electrical Engineering
Semester 1, 2004

COMP3601 - Software Specification

COMP7605 - Equivalent Course(s)

Course Profile


This is version 1.0 of the course profile, dated 10 February 2004.

Changes since the last version

Not applicable

Course Summary

Course Code(s):   COMP3601
Unit Value: #2
Contact Hours: 5 hours per week (3L2T)
Purpose: COMP3601 is intended to introduce students to a formal notation for specifying software systems and to the use of proof to validate such specifications

Teaching Staff

Dr Peter Robinson (Course Coordinator)
Office: 78-304
Phone: (07) 3365-3461
Fax: (07) 3365-4999
Email: pjr[at]itee.uq.edu.au



Course Goals

This course introduces students to the use of formal (mathematical) notation for specifying software systems. Formal specification notation allows for concise, unambiguous specification together with the ability to formally prove properties of the specification and to discover counterexamples to aid in the redesign of a specification.

It is expected that upon successful completion of the course, students will:

Graduate Attributes Developed

The University of Queensland has defined a set of graduate attributes to specify broad core knowledge and skills associated with all undergraduate programs (http://www.uq.edu.au/hupp/contents/view.asp?s1=3&s2=20&s3=5). This course addresses these attributes as follows:

Attribute Contributions from this Course
In-depth knowledge of the field of study  Formal specification, use of set theory and logic, proof, use of B-Tool
Effective Communication  Discussion of problems/issues in tutorials and on the newsgroup
Independence and Creativity  The use of the B-Tool allows students to be creative with their construction of specifications  and provides feedback so that this can be done in an independent way
Critical Judgment  The assignments and exam requires judgments about appropriate specification constructs and the analysis of specifications
Ethical and Social Understanding  Students are exposed to the idea that formal specifications can lead to the design of best-practice software, particularly in safety-critical areas, where software failure can lead to loss of life

Assumed Background

Pre: (COMP1500 or CS181) + (MATH1061 or MT161)
Inc: CS160 or 162 or 163 or 262 or 263 or COMP2600

Students are expected to have some background in programming and (informal) design as well as some knowledge of set theory and logic.


Course Profile Copy

In the first lecture students will be directed to the web address at which this course profile can be read.  Students enrolled at St Lucia who wish to retain a hard copy of the profile can use the free print quota provided each semester to students enrolled in courses in the School of Information Technology & Electrical Engineering.  For information on how to use this print quota, see the School Policy on Student Photocopying and Printing (St Lucia). Students enrolled at the Ipswich campus will either be provided with a hard copy or given directions in class on how to obtain a free copy.


The required text is

Steve Schneider, The B-Method: An Introduction, Palgrave, 2001.


All handouts will be made available on the COMP3601 web page.


Students will have access to the UNIX labs for running the B-Tool. Students can also obtain a license for running the B-Tool at home on LINUX (see course web page for details of obtaining a license). 


Peter Robinson has no specific consultation times but is happy to talk with students anytime the office door is open. Appointments can also be made via email or phone.

Distribution of Notices

Important notices will appear on the COMP3601 newsgroup and on the COMP3601 web pages. You are expected to read these notices regularly (at least once a week during semester and more often near assignment deadlines).


The course web site is available at http://www.itee.uq.edu.au/~comp3601 . The course web site will contain lecture slides, tutorial sheets and solutions, assignments, notices and other information relevant to the course.


The course newsgroup is uq.itee.comp3601 . This group is available on both the University and School news servers (news.uq.edu.au and news.itee.uq.edu.au).

Students are free to post questions (and answers!) to the newsgroup. Copies of announcements will also be posted to the newsgroup. The teaching staff will monitor the newsgroup and provide feedback as required.

Students should be careful about posting questions or answers directly related to assignments. If you are uncertain please contact the teaching staff.

Teaching Activities


There are two lecture times each week:
Lecture 1:
Tuesday 10-12 (room - TBA)
Lecture 2:
Thursday 12-1 (room - TBA)

Lecture 1 will run as a normal lecture (2 hrs with break). Lecture 2 will run more as a large tutorial - problems students are having will be discussed and more examples will be given. The intention is that this time will be used to revise and build on the material presented at the other lecture.
Experience suggests that students find lecture 2 very helpful for gaining a deeper understanding of the material.


Tutorials will be used to reinforce understanding of the course material. Selected problems from the textbook and elsewhere will be discussed. Active student participation is expected. One tutorial per week together with time in the lab will be enough for most students. However, students may attend more than one tutorial if they need more help.

The times for the tutorials will be discussed during the first lecture.


There are no designated prac sessions - the UNIX lab will be used in "open" mode for students to use the B-Tool for writing specifications.


You are not required to attend any of the teaching sessions (except those in which an assessment activity is taking place), however, you are strongly encouraged to do so. The lectures, tutorials and pracs have been specifically designed to aid your learning of the course material. Failure to attend a session may result in you being disadvantaged. It is up to you to find out what happened at any class session that you miss.

Teaching Plan

Week Number Monday's Date Lecture Topic Assessment
1 1 March Intro
B Machines
2 8 March
Set theory & Logic

Weakest preconditions
3 15 March Weakest preconditions
Consistency, Machine constructs
4 22 March Consistency
Relations, Functions, Sequences
5 29 March
Library Specification
6  April Structuring Specifications

12 April Mid-Semester Break
7 19 April Robust Machines

8 26 April Nondeterminism assignment 1 due

9 3 May Case studies

10 10 May
Case studies

11 17 May
Case studies

12 24 May
Comparison with other spec. languages assignment 2 due
13 31 May


The assessment for COMP3601 has two components:

  1. Two assignments each worth 20% of the total
  2. A final two-hour exam worth 60% of the total
The first assignment will be a modification of the library specification presented in lectures. The intention is to ease students into writing their own specifications. The second assignment will be about a complete specification of a system. Students are expected to use the B-Tool for developing their specifications: for type checking, proof obligation generation and pretty printing.
The exam will further test the students understanding of specification and their ability to produce specifications.


Both assignments are aimed at developing and testing students skills in specification and their use of proof to check for consistency of their specifications.

Assignment 1 - available week 3, due 9am 27 April (week 8)
Assignment 2 - available week 7, due 9am 25 May (week 12)

Marks for the assignments will be allocated according to the extent of the correctness of the submission.
Submissions with no academic merit will receive no marks.

Tutorial Exercises

Tutorials are aimed at developing students understanding of the use of set theory and logic for specification and how to use this to produce formal specifications. Although tutorials are not assessed, students are strongly advised to attempt the tutorial problems in order to develop their skills and to test their understanding.

Final Examination

A two hour final examination will be held during the final examination period. This exam will be open-book and will contain questions about specifications. Open-book means that you may bring any written material into the examination room. Calculators and other computing or communication devices are NOT permitted.
The examination will assess the students abilities to write specifications by turning informal descriptions into formal specification statements.  Marks for the examination will be allocated according to the extent of the correctness of the answers.

Determination of Final Grade

Your final mark will be calculated from the marks for the two assignments and the final exam as described earlier. Your final grade is then computed from the final mark using the following table.

final mark

1. Serious Fail
Fails to satisfy most or all of the basic requirements of the course.

2. Fail
Fails to satisfy some of the basic requirements of the course.

3. Pass Conceded
Falls short of satisfying all basic requirements for Pass but can be granted concession for deficiencies through:

  • being close to satisfactory overall, or

  • having compensating strengths in some aspects of the course, or

  • having compensating strengths in other courses, or

  • other mitigating considerations.

4. Pass
Satisfies all of the basic learning requirements for the course, such as knowledge of fundamental concepts and performance of basic skills; demonstrates sufficient quality of performance to be considered satisfactory or adequate or competent or capable in the course.

5. Credit
Demonstrates ability to use and apply fundamental concepts and skills of the course, going beyond mere replication of content knowledge or skill to show understanding of key ideas, awareness of their relevance, some use of analytical skills, and some originality or insight.

6. Distinction
Demonstrates awareness and understanding of deeper and subtler aspects of the course, such as ability to identify and debate critical issues or problems, ability to solve non-routine problems, ability to adapt and apply ideas to new situations, and ability to invent and evaluate new ideas.

7. High Distinction
Demonstrates imagination, originality or flair, based on proficiency in all the learning objectives for the course; work is interesting or surprising or exciting or challenging or erudite.

Each passing grade subsumes and goes beyond the grades lower than it.  At the discretion of the lecturers, final grades may be scaled upwards but not decreased.

Assessment Policies


The method for collection of assignments will be via the School electronic submission system . Details for submission will be specified on the assignment sheets and on the course web page.

Late Submission

Late submissions will attract a penalty of 20% per day or part thereof. If you are submitting an assignment late, you must inform the lecturer via email. Submissions will not be accepted more than one week late. Late submission are also submitted via the electronic submission system.

Return of Assignments

Assignments will be returned at tutorials or can be collected from the lecturer's room.

Academic Merit, Plagiarism, Proper Referencing, Collusion and Other Misconduct

The School and the wider academic community in general takes academic integrity and respect for other persons and property very seriously. In particular, the following behavior is unacceptable:

Penalties for engaging in unacceptable behaviour can range from cash fines or loss of grades in a subject, through to expulsion from the University.

You are required to read and understand the School Statement on Misconduct, available on the ITEE website at: http://www.itee.uq.edu.au/about_ITEE/policies/student-misconduct.html.  This Statement includes advice and links to other sites on how to properly cite references and other sources in your submissions and on acceptable levels of collaboration.

If you have any questions concerning this statement, please contact your lecturer in the first instance.

Assessment Feedback

Timely feedback on all progressive assessment in this course will be available in accordance with University policy (HUPP 3.30.6 Student Access to Feedback on Assessment). 

Assignments will be marked in the week following the due date. After marking is complete, the scripts (with written feedback) will be available from the following tutorial and subsequently at the lecturer's office. Students are strongly encouraged to retrieve their marked scripts and discuss any problems with the lecturer or tutor with the aim of correcting any misunderstandings before the next piece of assessment is due.

The lecturer will provide general feedback in lectures following the completion of marking.

Students wishing to view examination answer scripts and/or question papers should consult with the School office (Room 217, General Purpose South Building [78], St Lucia;  Room 218, Building 1, Ipswich) regarding arrangements.

It is a student’s responsibility to incorporate feedback into their learning; making use of the assessment criteria that they are given; being aware of the rules, policies and other documents related to assessment; and providing teachers with feedback on their assessment practices.

Support for Students with a Disability

Any student with a disability who may require alternative academic arrangements in the course is encouraged to seek advice at the commencement of the semester from a Disability Adviser at Student Support Services.

Sourced From http://www.itee.uq.edu.au/undergraduate/_profile_view.php?print=1&file=2004_1_COMP3601_StLucia