Assignment 3 CSSE3100/7100 Reasoning about Programs
Due: 4pm on 19 May, 2023
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 a Dafny file with your solutions to Question 1 to Gradescope by
the due date and time.
1. In a program that you are developing, you have a number of items arriving that need
processing. The items fall into two categories, each requiring processing in a specific way.
Hence, you decide to use two stacks, s1 and s2, for storing the items. The most items you will
need to have in both stacks at any time is N. Since you don't know in advance how many
items there will be of each category, your stacks would need to be each of size N.
Alternatively, for space efficiency you could use a single array of size N with s1 growing
from the front of the array, and s2 growing from the end.
Write a Dafny class TwoStacks, where T is the type of the items, which uses the
alternative design above but hides the design from the user: the specification should only
refer to s1, s2, N and Repr (if required). The class should offer the methods push1 and push2,
for pushing items onto the top of s1 and s2 respectively, and pop1 and pop2 for popping (i.e.,
returning and removing) items from the top of s1 and s2 respectively. These methods should
always be enabled with the push methods returning the value false when the array is full (and
true otherwise), and the pop methods returning false along with an arbitrary value of type T
when the array is empty (and true and the popped item otherwise). Note: you can assign an
arbitrary value to a variable x with x := *; in Dafny.
Additionally, there should be:
• Methods peek1 and peek2 for returning the top item of the relevant stack without
removing it from the stack. Like the pop methods, these methods should return false
along with an arbitrary value of type T when the array is empty (and true and the top
item otherwise).
• Predicates empty1 and empty2 that return true when the relevant stack is empty.
• Methods search1 and search2 which take an item as an argument, and return the
position of that item in the relevant stack, or -1 when the item is not in the stack. Note
the position in the stack should be of the occurrence of the item nearest the top of the
stack, and should be 1-based, meaning the item at the top of the stack is in position 1.
Throughout your class, you must follow the style of specification we have been using for
objects and data structures in the lectures. The corresponding methods of each stack must be
specified identically apart from references to s1 and s2.
Hints: Make sure you don't underspecify. Think about all constraints that the constructor,
each method and each predicate needs to ensure.
top of s1 top of s2
0 N
Marking
You will get marks for
• correctness of specifications
• completeness of specifications
• key lines of code
• correctness and completeness of loop invariants
Note that you will get part marks even if your code doesn't verify in Dafny.
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