2024年6月20日

CS代写｜CSSE3100/7100 Reasoning about Programs Assignment 3

这是一个CS Assignment代写的相关案例

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.

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. 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.

[2 marks]

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.