-CSSE3100/7100

Assignment 3 CSSE3100/7100 Reasoning about Programs

Due: 4pm on 17 May, 2024

The aim of this assignment is to consolidate your understanding of the course's material on objects

and array-based data structures. It is worth 15% of your final mark for the course.

Instructions: Upload the provided Dafny file A3.dfy extended with your solution for Question 1

(and Question 2) if applicable to Gradescope by the due date and time.

1. The provided file A3.dfy contains skeletons for two Dafny classes. Your task is to provide verified

implementations for these classes following the approach detailed in the lectures. Stack will be a

bounded stack and Queue a bounded queue.https://weibo.com/u/7915668133

You should start your task by providing complete specifications of the desired behaviour of the

classes. The desired behaviour of a stack is that it is a last-in, first-out (LIFO) collection of values,

whereas the desired behaviour of a queue is that it is a first-in, first-out (FIFO) collection of values.

Since the data structures are bounded, their specifications should reflect that values can be added to

them only when they are not full, and removed from them only when they are not empty. (In

particular, you do not need to return a special 'None' value for the empty case.)

The class Stack should be implemented using a single array, and other variables (which are neither

objects nor arrays) as required. The class Queue should be implemented using two objects of class

Stack called stack1 and stack2 (and no other variables). Each of the stacks should have the same

maximum size as the queue. Values added to the queue will be pushed onto stack1, and values

removed from the queue will be popped from stack2. If stack2 is empty when a pop is required, all

elements of stack1 will first be popped and pushed onto stack2, so that they appear in stack2 in the

reverse order to the order they were originally pushed onto stack1.

To move the elements from stack1 to stack2, the Remove method of Queue will require a loop and

hence a loop invariant. Make sure your loop invariant implies the method's postcondition when the

loop guard is false. Think about the loop design techniques to ensure this. If needed, you may define

additional ghost predicates to use in your invariant to reduce complexity. [15 marks]

2. CSSE7100 students only. Add an extra method, Peek, and its specification to Queue. The Peek

method returns the same element as Remove but does not remove it from the queue.

You must not change the Stack class to do this. Instead Peek should call Remove to get and remove

the element from stack2, and then should push that element back onto stack2. [2 marks]

Marking

You will get marks for

• correctness and completeness of specifications following the approach in lectures

• correctness and completeness of the loop invariant

• code which verifies in Dafny.

Note that you will get part marks even if your code doesn't verify in Dafny.

For CSSE7100 students, the final mark is M + (m - 2) where M is the mark for Question 1 (out of 15)

and m is the mark for Question 2 (out of 2). The mark you will see on Gradescope for Question 2 will

be (m - 2). Note that this will be 0 for m = 2 and negative for a mark less than 2.

Copyright Notice © This content is protected and may not be shared, uploaded or distributed. The School of EECS at the University of Queensland

holds the copyright for this material. Students are not permitted to share these materials on sites external to the University of Queensland.

School Policy on Student Misconduct

This assignment is to be completed individually. You are required to read and understand the School

Statement on Misconduct, available on the School's website at: http://www.itee.uq.edu.au/itee-

student-misconduct-including-plagiarism

This assessment task evaluates students' abilities, skills and knowledge without the aid of generative

Artificial Intelligence (AI). Students are advised that the use of AI technologies to develop responses

is strictly prohibited and may constitute student misconduct under the Student Code of Conduct.

Copyright Notice © This content is protected and may not be shared, uploaded or distributed. The School of EECS at the University of Queensland

holds the copyright for this material. Students are not permitted to share these materials on sites external to the University of Queensland.