Course coordinator
Associate Professor Graeme Smith
Course overview
- Study period
- Semester 1, 2025 (24/02/2025 - 21/06/2025)
- Study level
- Undergraduate
- Location
- St Lucia
- Attendance mode
- In Person
- Units
- 2
- Administrative campus
- St Lucia
- Coordinating unit
- Elec Engineering & Comp Science School
Software is written with the intention that it will carry out a desired task. To write such software requires algorithmic problem solving skills; and to do so correctly requires us to make precise the task at hand, and to be able to reason that an implementation satisfies the task's precise requirements. This advanced course on programming introduces structured, formal methods for: specifying the desired behaviour of programs, showing that programs are correct with respect to their specifications, and deriving algorithms from specifications. These techniques are designed to assist developers to solve programming problems, and to produce high quality software.
The primary aim of this course is to introduce you to techniques and tools that allow you to reason about a program to show that it meets its specification for all valid inputs, not just a single test input. In other words, you will learn to verify that a program satisfies its specification.
On entry to Reasoning About Programs, you will have studied basic programming techniques as well as proofs in predicate logic. The course brings these two strands of study together to use logic to reason about programs. You will also learn to use state-of-the-art tools for automating and checking proofs of program correctness.
Overall, this course can be viewed as an advanced course on programming, with the emphasis being on developing your ability to guarantee that a program you have written satisfies its specification.
In response to previous student feedback, the problem-based learning sessions in this course have been extended from 1 to 2 hours (to provide students with more access to teaching staff on a weekly basis). Also, new lecture material has been added on debugging failed verification attempts (to aid students with using the program verifier in assignments).
Course requirements
Assumed background
Students are expected to have done at least 2 programming courses including one covering object orientation (e.g. CSSE1001 and CSSE2002), and to have a solid understanding of predicate logic.
Prerequisites
You'll need to complete the following courses before enrolling in this one:
MATH1061 and CSSE2002
Incompatible
You can't enrol in this course if you've already completed the following:
CSSE7100
Jointly taught details
This course is jointly-taught with:
- CSSE7100
Course contact
Course staff
Lecturer
Associate Professor Graeme Smith
Timetable
The timetable for this course is available on the UQ Public Timetable.
Aims and outcomes
To enhance your ability to program by teaching you an alternative approach to designing algorithms that will deepen your understanding of how to think about programs.
To develop skills in both specifying programs and reasoning about the correctness of programs, with the aim of being able to derive correct programs from specifications.
To give you experience using state-of-the-art program verification tools.
Learning outcomes
After successfully completing this course you should be able to:
LO1.
Explain the rationale for the formal specification and verification of programs.
LO2.
Specify the desired behaviour of methods and functions in a program in a mathematically precise way.
LO3.
Use formal techniques to verify that a method is correct with respect to its specification.
LO4.
Derive correct methods from abstract specifications using a formal, structured approach.
LO5.
Specify and verify the correctness of objects and data structures in programs.
LO6.
Use a verification tool to automatically and interactively verify the correctness of programs.
Assessment
Assessment summary
| Category | Assessment task | Weight | Due date |
|---|---|---|---|
| Computer Code | Assignment 1 | 15% |
1/04/2025 4:00 pm |
| Computer Code | Assignment 2 | 20% |
6/05/2025 4:00 pm |
| Computer Code | Assignment 3 | 15% |
27/05/2025 4:00 pm |
| Examination |
Final exam
|
50% |
End of Semester Exam Period 7/06/2025 - 21/06/2025 |
A hurdle is an assessment requirement that must be satisfied in order to receive a specific grade for the course. Check the assessment details for more information about hurdle requirements.
Assessment details
Assignment 1
- Mode
- Written
- Category
- Computer Code
- Weight
- 15%
- Due date
1/04/2025 4:00 pm
- Learning outcomes
- L01, L02, L03
Task description
Students will formally verify one or more programs using weakest precondition reasoning.
This assessment task evaluates students' abilities, skills and knowledge without the aid of generative Artificial Intelligence (AI) or Machine Translation (MT). Students are advised that the use of AI or MT technologies to develop responses is strictly prohibited and may constitute student misconduct under the Student Code of Conduct.
Submission guidelines
Assignments are to be submitted electronically via Gradescope.
Deferral or extension
You may be able to apply for an extension.
The maximum extension allowed is 7 days. Extensions are given in multiples of 24 hours.
This course uses a progressive assessment approach where feedback and/or detailed solutions will be released to students within 14 days.
Late submission
A penalty of 10% of the maximum possible mark will be deducted per 24 hours from time submission is due for up to 7 days. After 7 days, you will receive a mark of 0.
Assignment 2
- Mode
- Written
- Category
- Computer Code
- Weight
- 20%
- Due date
6/05/2025 4:00 pm
- Learning outcomes
- L01, L02, L03, L04, L06
Task description
Students will formally specify and derive one or more programs, and verify them using the Dafny verification tool.
This assessment task evaluates students' abilities, skills and knowledge without the aid of generative Artificial Intelligence (AI) or Machine Translation (MT). Students are advised that the use of AI or MT technologies to develop responses is strictly prohibited and may constitute student misconduct under the Student Code of Conduct.
Submission guidelines
Assignments are to be submitted electronically via Gradescope.
Deferral or extension
You may be able to apply for an extension.
The maximum extension allowed is 7 days. Extensions are given in multiples of 24 hours.
This course uses a progressive assessment approach where feedback and/or detailed solutions will be released to students within 14 days.
Late submission
A penalty of 10% of the maximum possible mark will be deducted per 24 hours from time submission is due for up to 7 days. After 7 days, you will receive a mark of 0.
Assignment 3
- Mode
- Written
- Category
- Computer Code
- Weight
- 15%
- Due date
27/05/2025 4:00 pm
- Learning outcomes
- L01, L02, L03, L05, L06
Task description
Students will formally specify one or more programs using objects and data structures, and verify them using the Dafny verification tool.
This assessment task evaluates students' abilities, skills and knowledge without the aid of generative Artificial Intelligence (AI) or Machine Translation (MT). Students are advised that the use of AI or MT technologies to develop responses is strictly prohibited and may constitute student misconduct under the Student Code of Conduct.
Submission guidelines
Assignments are to be submitted electronically via Gradescope.
Deferral or extension
You may be able to apply for an extension.
The maximum extension allowed is 7 days. Extensions are given in multiples of 24 hours.
This course uses a progressive assessment approach where feedback and/or detailed solutions will be released to students within 14 days.
Late submission
A penalty of 10% of the maximum possible mark will be deducted per 24 hours from time submission is due for up to 7 days. After 7 days, you will receive a mark of 0.
Final exam
- Hurdle
- Identity Verified
- In-person
- Mode
- Written
- Category
- Examination
- Weight
- 50%
- Due date
End of Semester Exam Period
7/06/2025 - 21/06/2025
- Other conditions
- Time limited.
- Learning outcomes
- L01, L02, L03, L04, L05
Task description
A two-hour final examination will be held during the final examination period. The examination is used to assess both the practical ability of the students on small problems and their understanding of the course material.
You may bring in one A4-size page crib sheet written or printed on both sides; no other written or printed material is permitted. Calculators and other computing or communication devices are not permitted.
Hurdle requirements
If you fail to obtain at least 50% of the mark for the final exam (i.e. 25 out of 50), your overall mark will be capped at 49%, corresponding to an overall grade of 3 or lower. If you fail to obtain at least 40% of the mark for the final exam (i.e. 20 out of 50), your overall mark will be capped at 46%, corresponding to an overall grade of 2 or lower.Exam details
| Planning time | 10 minutes |
|---|---|
| Duration | 120 minutes |
| Calculator options | No calculators permitted |
| Open/closed book | Closed Book examination - specified written materials permitted |
| Materials | One A4 sheet of handwritten or typed notes, double sided, is permitted |
| Exam platform | Paper based |
| Invigilation | Invigilated in person |
Submission guidelines
Deferral or extension
You may be able to defer this exam.
Course grading
Full criteria for each grade is available in the Assessment Procedure.
| Grade | Cut off Percent | Description |
|---|---|---|
| 1 (Low Fail) | 0 - 19 |
Absence of evidence of achievement of course learning outcomes. |
| 2 (Fail) | 20 - 46 |
Minimal evidence of achievement of course learning outcomes. |
| 3 (Marginal Fail) | 47 - 49 |
Demonstrated evidence of developing achievement of course learning outcomes |
| 4 (Pass) | 50 - 64 |
Demonstrated evidence of functional achievement of course learning outcomes. |
| 5 (Credit) | 65 - 74 |
Demonstrated evidence of proficient achievement of course learning outcomes. |
| 6 (Distinction) | 75 - 84 |
Demonstrated evidence of advanced achievement of course learning outcomes. |
| 7 (High Distinction) | 85 - 100 |
Demonstrated evidence of exceptional achievement of course learning outcomes. |
Additional course grading information
Your final mark will be calculatedﾠ by adding upﾠ your marks for the assignments (out of 50), and the final exam (out of 50). If you fail to obtain at least 50% of the mark for the final exam (i.e. 25 out of 50), your overall mark will be capped at 49%, corresponding to an overall grade of 3 or lower. If you fail to obtain at least 40% of the mark for the final exam (i.e. 20 out of 50), your overall mark will be capped at 46%, corresponding to an overall grade of 2 or lower.
The final mark will be rounded to the nearest whole number before grade cutoffs apply. At the discretion of the course coordinator,ﾠ marks forﾠ assessment itemsﾠ may be adjustedﾠ upwards (uniformly across the class), but not downwards.
Supplementary assessment
Supplementary assessment is available for this course.
Additional assessment information
Having Troubles?
If you are having difficulties with any aspect of the course material you should seek help. Speak to a member of the teaching team.
If external circumstances are affecting your ability to work on the course, you should seek help as soon as possible. The University and UQ Union have organisations and staff who are able to help, for example, UQ Student Services are able to help with study and exam skills, tertiary learning skills, writing skills, financial assistance, personal issues, and disability services (among other things).
Complaints and criticisms should be directed in the first instance to the course coordinator. If you are not satisfied with the outcome, you may bring the matter to the attention of the Director of Teaching and Learning.
Learning resources
You'll need the following resources to successfully complete the course. We've indicated below if you need a personal copy of the reading materials or your own item.
Library resources
Find the required and recommended resources for this course on the UQ Library website.
Additional learning resources information
Dafny program verifier
The Dafny program verifier will be used in this course. Instructions for installing it in VSCode on Windows, Mac and Linux can be found at https://dafny.org/dafny/Installation#Visual-Studio-Code
Handouts
Electronic copies of all handouts will be made available on the course Blackboard site.
Distribution of notices
Announcements will be made in the lectures and on the course Blackboard site. You are expected to read the notices on the course Blackboard site (at least once a week and more often near assignment deadlines).
Learning activities
The learning activities for this course are outlined below. Learn more about the learning outcomes that apply to this course.
Filter activity type by
Please select
| Learning period | Activity type | Topic |
|---|---|---|
Multiple weeks From Week 1 To Week 13 |
Lecture |
Lectures Lectures will be used to introduce new course content. Learning outcomes: L01, L02, L03, L04, L05, L06 |
Problem-based learning |
Problem-based learning sessions These sessions will be used to work on exercises on the course content, and to get help with assignments. Learning outcomes: L01, L02, L03, L04, L05, L06 |
Policies and procedures
University policies and procedures apply to all aspects of student life. As a UQ student, you must comply with University-wide and program-specific requirements, including the:
- Student Code of Conduct Policy
- Student Integrity and Misconduct Policy and Procedure
- Assessment Procedure
- Examinations Procedure
- Reasonable Adjustments - Students Policy and Procedure
Learn more about UQ policies on my.UQ and the Policy and Procedure Library.
School guidelines
Your school has additional guidelines you'll need to follow for this course: