UQ Students should read the Disclaimer & Warning
Note: This page dates from 2005, and is kept for historical purposes.
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<!-- saved from url=(0094)http://www.itee.uq.edu.au/undergraduate/_profile_view.php?print=1&file=2004_1_COMP3601_StLucia -->
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<title>COMP3601 – Course Profile</title>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<meta
content="School of Information Technology and Electrical Engineering - Course Profile"
name="Description" />
</head>
<body bgcolor="#ffffff">
<h3 align="center">The University of Queensland<br />
School of Information Technology and Electrical Engineering<br />
Semester 1, 2004<br />
</h3>
<h1 align="center" ?="">COMP3601 - Software Specification</h1>
<h1 align="center" ?="">COMP7605 - Equivalent Course(s)</h1>
<h1 align="center">Course Profile</h1>
<h2>Version</h2>
<p>This is version 1.0 of the course profile, dated <b>10 February 2004</b>.</p>
<h3>Changes since the last version</h3>
<p>Not applicable<br />
</p>
<hr />
<h2>Course Summary</h2>
<table id="AutoNumber6"
bordercolor="#111111" cellspacing="1" cellpadding="3" border="1">
<tbody>
<tr>
<td nowrap="nowrap"><b>Course Code(s):</b></td>
<td><b> </b>COMP3601</td>
</tr>
<tr>
<td nowrap="nowrap"><b>Unit Value:</b></td>
<td>#2</td>
</tr>
<tr>
<td nowrap="nowrap"><b>Contact Hours:</b></td>
<td>5 hours per week (3L2T)</td>
</tr>
<tr>
<td nowrap="nowrap"><b>Purpose:</b></td>
<td>COMP3601 is intended to introduce students to a formal notation for specifying
software systems and to the use of proof to validate such specifications</td>
</tr>
</tbody>
</table>
<hr />
<h2>Teaching Staff</h2>
<p><b>Dr Peter Robinson (Course Coordinator)</b><br />
Office: 78-304<br />
Phone: (07) 3365-3461<br />
Fax: (07) 3365-4999<br />
Email: pjr[at]itee.uq.edu.au <br />
</p>
<h3>Tutors</h3>
<p>TBA<br />
</p>
<hr />
<h2>Course Goals</h2>
<p>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.</p>
<p>It is expected that upon successful completion of the course, students will:</p>
<ul>
<li>understand the use of set theory and logic for specifying software systems, </li>
<li>know how to apply set theory and logic to the problem of specification and
to carry out proofs and find counterexamples, and </li>
<li>be able to specify small to medium sized software systems and to be able
to (informally) prove properties about the specifications. </li>
</ul>
<h2>Graduate Attributes Developed</h2>
<p>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:</p>
<table id="AutoNumber4"
bordercolor="#111111" height="96" cellspacing="1" width="100%" border="1">
<tbody>
<tr>
<th width="20%" height="16">Attribute</th>
<th width="80%" height="16">Contributions from this Course</th>
</tr>
<tr>
<td width="20%" height="16">In-depth knowledge of the field of study</td>
<td width="80%" height="16"> Formal specification, use of set theory
and logic, proof, use of B-Tool</td>
</tr>
<tr>
<td width="20%" height="19">Effective Communication</td>
<td width="80%" height="19"> Discussion of problems/issues in tutorials
and on the newsgroup</td>
</tr>
<tr>
<td width="20%" height="19">Independence and Creativity</td>
<td width="80%" height="19"> 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</td>
</tr>
<tr>
<td width="20%" height="19">Critical Judgment</td>
<td width="80%" height="19"> The assignments and exam requires judgments
about appropriate specification constructs and the analysis of specifications</td>
</tr>
<tr>
<td width="20%" height="19">Ethical and Social Understanding</td>
<td width="80%" height="19"> 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</td>
</tr>
</tbody>
</table>
<hr />
<hr />
<h2>Assumed Background</h2>
<p>Pre: (COMP1500 or CS181) + (MATH1061 or MT161)<br />
Inc: CS160 or 162 or 163 or 262 or 263 or COMP2600<br />
</p>
<p>Students are expected to have some background in programming and (informal)
design as well as some knowledge of set theory and logic.</p>
<hr />
<h2>Resources</h2>
<h3>Course Profile Copy</h3>
<p>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.</p>
<h3>Textbook</h3>
<p>The required text is</p>
<blockquote>
<p>Steve Schneider, <b>The B-Method: An Introduction</b>, Palgrave, 2001.</p>
</blockquote>
<h3>Handouts</h3>
<p>All handouts will be made available on the COMP3601 web page.</p>
<h3>Facilities</h3>
<p>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). </p>
<h3>Consultation</h3>
<p>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.<br />
</p>
<h3>Distribution of Notices</h3>
<p>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).<br />
<br />
</p>
<h3>Web<br />
</h3>
<p>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.<br />
</p>
<h3>Newsgroup</h3>
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).
<p>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.<br />
</p>
<p>Students should be careful about posting questions or answers directly related
to assignments. If you are uncertain please contact the teaching staff.</p>
<h2>Teaching Activities</h2>
<h3>Lectures<br />
</h3>
<dl>
<dt><br />
</dt>
<dt>There are two lecture times each week: </dt>
<dt>Lecture 1: </dt>
<dd>Tuesday 10-12 (room - TBA) </dd>
<dt>Lecture 2: </dt>
<dd>Thursday 12-1 (room - TBA)<br />
<br />
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. </dd>
</dl>
Experience suggests that students find lecture 2 very helpful for gaining a deeper
understanding of the material.<br />
<h3>Tutorials</h3>
<p>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.<br />
</p>
<p>The times for the tutorials will be discussed during the first lecture.</p>
<h3>Pracs</h3>
<p>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.<br />
</p>
<h3>Attendance</h3>
<p>You are not <i>required</i> to attend any of the teaching sessions (except
those in which an assessment activity is taking place), however, you are <i>strongly
encouraged</i> 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.</p>
<h3>Teaching Plan</h3>
<table
bordercolor="#111111" cellspacing="1" border="1">
<tbody>
<tr>
<th width="102">Week Number</th>
<th width="155">Monday's Date</th>
<th width="400">Lecture Topic</th>
<th width="197">Assessment</th>
</tr>
<tr>
<td align="middle" width="102" rowspan="2">1</td>
<td align="middle" width="155" rowspan="2">1 March</td>
<td width="400">Intro </td>
<td width="197" rowspan="2"><br /></td>
</tr>
<tr>
<td width="400">B Machines</td>
</tr>
<tr>
<td align="middle" width="102" rowspan="2">2</td>
<td align="middle" width="155" rowspan="2">8 March<br /></td>
<td width="400">Set theory & Logic<br /></td>
<td width="197" rowspan="2"><br /></td>
</tr>
<tr>
<td width="400">Weakest preconditions</td>
</tr>
<tr>
<td align="middle" width="102" rowspan="2">3</td>
<td align="middle" width="155" rowspan="2">15 March</td>
<td width="400">Weakest preconditions</td>
<td width="197" rowspan="2"><br /></td>
</tr>
<tr>
<td width="400">Consistency, Machine constructs</td>
</tr>
<tr>
<td align="middle" width="102" rowspan="2">4</td>
<td align="middle" width="155" rowspan="2">22 March</td>
<td width="400">Consistency</td>
<td width="197" rowspan="2"><br /></td>
</tr>
<tr>
<td width="400">Relations, Functions, Sequences</td>
</tr>
<tr>
<td align="middle" width="102" rowspan="2">5</td>
<td align="middle" width="155" rowspan="2">29 March<br /></td>
<td width="400">Library Specification</td>
<td width="197" rowspan="2"><br /></td>
</tr>
<tr>
<td width="400">Proofs</td>
</tr>
<tr>
<td align="middle" width="102" rowspan="2">6</td>
<td align="middle" width="155" rowspan="2"> April</td>
<td width="400">Structuring Specifications</td>
<td width="197" rowspan="2"><br /></td>
</tr>
<tr>
<td width="400"><br /></td>
</tr>
<tr></tr>
<tr>
<td align="middle" width="102"><br /></td>
<td align="middle" width="155">12 April</td>
<td align="middle" width="400" colspan="2">Mid-Semester Break<br /></td>
</tr>
<tr>
<td align="middle" width="102" rowspan="2">7</td>
<td align="middle" width="155" rowspan="2">19 April</td>
<td width="400">Robust Machines</td>
<td width="197" rowspan="2"><br /></td>
</tr>
<tr>
<td width="400"><br /></td>
</tr>
<tr>
<td align="middle" width="102" rowspan="2">8</td>
<td align="middle" width="155" rowspan="2">26 April</td>
<td width="400">Nondeterminism </td>
<td width="197" rowspan="2">assignment 1 due<br /></td>
</tr>
<tr>
<td width="400"><br /></td>
</tr>
<tr>
<td align="middle" width="102" rowspan="2">9</td>
<td align="middle" width="155" rowspan="2">3 May</td>
<td width="400">Case studies</td>
<td width="197" rowspan="2"><br /></td>
</tr>
<tr>
<td width="400"><br /></td>
</tr>
<tr>
<td align="middle" width="102" rowspan="2">10</td>
<td align="middle" width="155" rowspan="2">10 May<br /></td>
<td width="400">Case studies </td>
<td width="197" rowspan="2"><br /></td>
</tr>
<tr>
<td width="400"><br /></td>
</tr>
<tr>
<td align="middle" width="102" rowspan="2">11</td>
<td align="middle" width="155" rowspan="2">17 May<br /></td>
<td width="400">Case studies </td>
<td width="197" rowspan="2"><br /></td>
</tr>
<tr>
<td width="400"><br /></td>
</tr>
<tr>
<td align="middle" width="102" rowspan="2">12</td>
<td align="middle" width="155" rowspan="2">24 May<br /></td>
<td width="400">Comparison with other spec. languages</td>
<td width="197" rowspan="2">assignment 2 due<br /></td>
</tr>
<tr>
<td width="400"> </td>
</tr>
<tr>
<td align="middle" width="102" rowspan="2">13</td>
<td align="middle" width="155" rowspan="2">31 May<br /></td>
<td width="400">Revision </td>
<td width="197" rowspan="2"><br /></td>
</tr>
<tr>
<td width="400"><br /></td>
</tr>
</tbody>
</table>
<br />
<h2>Assessment</h2>
<p>The assessment for COMP3601 has two components:<br />
</p>
<ol>
<li>Two assignments each worth 20% of the total </li>
<li>A final two-hour exam worth 60% of the total </li>
</ol>
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.<br />
The exam will further test the students understanding of specification and their
ability to produce specifications.<br />
<br />
<h3>Assignments</h3>
<p>Both assignments are aimed at developing and testing students skills in specification
and their use of proof to check for consistency of their specifications. <br />
</p>
<p>Assignment 1 - available week 3, due 9am 27 April (week 8)<br />
Assignment 2 - available week 7, due 9am 25 May (week 12)<br />
</p>
<p>Marks for the assignments will be allocated according to the extent of the
correctness of the submission.<br />
Submissions with no academic merit will receive no marks.<br />
</p>
<h3>Tutorial Exercises<br />
</h3>
<p>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.<br />
</p>
<h3>Final Examination</h3>
<p>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 <i>written</i> material into the examination
room. Calculators and other computing or communication devices are NOT permitted. <br />
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.<br />
</p>
<h3>Determination of Final Grade</h3>
<p>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.<br />
<br />
</p>
<table width="200" border="1" cellpadding="2" cellspacing="0" bordercolor="#000000">
<tbody>
<tr>
<td valign="top" align="middle" width="30"><b>final mark</b><br /></td>
<td valign="top" align="middle" width="30"><b>grade</b><br /></td>
</tr>
<tr>
<td valign="top" align="middle">85-100<br /></td>
<td valign="top" align="middle">7<br /></td>
</tr>
<tr>
<td valign="top" align="middle">75-84<br /></td>
<td valign="top" align="middle">6<br /></td>
</tr>
<tr>
<td valign="top" align="middle">65-74<br /></td>
<td valign="top" align="middle">5<br /></td>
</tr>
<tr>
<td valign="top" align="middle">50-64<br /></td>
<td valign="top" align="middle">4<br /></td>
</tr>
<tr>
<td valign="top" align="middle">45-49<br /></td>
<td valign="top" align="middle">3<br /></td>
</tr>
<tr>
<td valign="top" align="middle">20-44<br /></td>
<td valign="top" align="middle">2<br /></td>
</tr>
<tr>
<td valign="top" align="middle">0-19<br /></td>
<td valign="top" align="middle">1<br /></td>
</tr>
</tbody>
</table>
<br />
<blockquote>
<p style="MARGIN-TOP: 0px; MARGIN-BOTTOM: 0px"><b>1. </b><i>Serious Fail</i> <br />
Fails to satisfy most or all of the basic requirements of the course. </p>
<p style="MARGIN-TOP: 0px; MARGIN-BOTTOM: 0px"><br />
<b>2. </b><i>Fail</i> <br />
Fails to satisfy some of the basic requirements of the course. </p>
<p style="MARGIN-TOP: 0px; MARGIN-BOTTOM: 0px"><br />
<b>3. </b><i>Pass Conceded</i> <br />
Falls short of satisfying all basic requirements for Pass but can be
granted concession for deficiencies through: </p>
<blockquote>
<ul>
<li>
<p style="MARGIN-TOP: 0px; MARGIN-BOTTOM: 0px">being close to satisfactory
overall, or </p>
</li>
<li>
<p style="MARGIN-TOP: 0px; MARGIN-BOTTOM: 0px">having compensating strengths
in some aspects of the course, or </p>
</li>
<li>
<p style="MARGIN-TOP: 0px; MARGIN-BOTTOM: 0px">having compensating strengths
in other courses, or </p>
</li>
<li>
<p style="MARGIN-TOP: 0px; MARGIN-BOTTOM: 0px">other mitigating considerations. </p>
</li>
</ul>
</blockquote>
<p style="MARGIN-TOP: 0px; MARGIN-BOTTOM: 0px"><b>4. </b><i>Pass</i> <br />
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. <br />
<br />
<b>5. </b><i>Credit</i> <br />
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. <br />
<br />
<b>6. </b><i>Distinction</i> <br />
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. <br />
<br />
<b>7. </b><i>High Distinction</i> <br />
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. </p>
</blockquote>
<p style="MARGIN-TOP: 0px; MARGIN-BOTTOM: 0px">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. </p>
<br />
<hr />
<h2>Assessment Policies</h2>
<h3>Submission</h3>
<p>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.<br />
</p>
<h3>Late Submission</h3>
<p>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.<br />
</p>
<h3>Return of Assignments</h3>
<p>Assignments will be returned at tutorials or can be collected from the lecturer's
room.<br />
</p>
<h3>Academic Merit, Plagiarism, Proper Referencing, Collusion and Other Misconduct</h3>
<p>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: </p>
<ul>
<li>Submission of plagiarised work, i.e. work that contains content copied from
an unacknowledged source. </li>
<li>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. </li>
<li>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. </li>
<li>Copying work done by other students. </li>
<li>Failing to adhere to the School's regulations concerning behaviour in laboratories,
in particular occupational health and safety regulations. </li>
</ul>
<p>Penalties for engaging in unacceptable behaviour can range from cash fines
or loss of grades in a subject, through to expulsion from the University.<br />
<br />
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. <br />
<br />
If you have any questions concerning this statement, please contact your
lecturer in the first instance.</p>
<h3>Assessment Feedback</h3>
<p>Timely feedback on all progressive assessment in this course will be available
in accordance with University policy (HUPP 3.30.6 <i>Student Access to Feedback
on Assessment</i>). <br />
<br />
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.<br />
<br />
The lecturer will provide general feedback in lectures following the completion
of marking. </p>
<p>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.</p>
<p>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.</p>
<hr />
<h2>Support for Students with a Disability</h2>
<p>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. </p>
<hr />
<p>Sourced From <a href="http://www.itee.uq.edu.au/undergraduate/_profile_view.php?print=1&file=2004_1_COMP3601_StLucia">http://www.itee.uq.edu.au/undergraduate/_profile_view.php?print=1&file=2004_1_COMP3601_StLucia</a></p>
</body>
</html>