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
Version
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
Tutors
TBA
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:
- understand the use of set theory and logic for specifying software systems,
- know how to apply set theory and logic to the problem of specification and to carry out proofs and find counterexamples, and
- be able to specify small to medium sized software systems and to be able to (informally) prove properties about the specifications.
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.
Resources
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.
Textbook
The required text is
Steve Schneider, The B-Method: An Introduction, Palgrave, 2001.
Handouts
All handouts will be made available on the COMP3601 web page.
Facilities
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).
Consultation
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).
Web
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.
Newsgroup
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
Lectures
- 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.
Tutorials
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.
Pracs
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.
Attendance
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 | |
| Proofs | |||
| 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 |
Revision | |
Assessment
The assessment for COMP3601 has two components:
- Two assignments each worth 20% of the total
- A final two-hour exam worth 60% of the total
The exam will further test the students understanding of specification and their ability to produce specifications.
Assignments
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 |
grade |
| 85-100 |
7 |
| 75-84 |
6 |
| 65-74 |
5 |
| 50-64 |
4 |
| 45-49 |
3 |
| 20-44 |
2 |
| 0-19 |
1 |
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
Submission
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:
- Submission of plagiarised work, i.e. work that contains content copied from an unacknowledged source.
- Submission of work without academic merit, i.e. work that adds little or nothing to material available from reference sources such as textbooks, websites, etc., even where this is appropriately acknowledged.
- Engaging in collusive behaviour, i.e. inappropriate working together with other students where individual work is required, or working with people outside your team where team work is required.
- Copying work done by other students.
- Failing to adhere to the School's regulations concerning behaviour in laboratories, in particular occupational health and safety regulations.
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