Skip to menu Skip to content Skip to footer
Course profile

Reasoning About Programs (CSSE3100)

Study period
Sem 1 2025
Location
St Lucia
Attendance mode
In Person

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
  • Hurdle
  • Identity Verified
  • In-person
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.

See the conditions definitions

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
Clear filters
Learning period Activity type Topic
Multiple weeks

From Week 1 To Week 13
(24 Feb - 01 Jun)

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:

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: