CSSE3100/7100 Reasoning About Programs - Semester One 2020- Final Exam - Q7 Bounded Queue
QUESTION 7
A bounded queue is a sequence of up to N elements where users can insert elements one at a time, and then remove them one at a time in the same order that they were inserted. For example, if the user inserted the element A, then B, then C, they would rst remove A, then B, and so on.
One way to implement a bounded queue is with an array and two pointers, in and out, to array indicies. Elements are inserted at array index, in, and removed at array index, out. That is, in denotes the rst empty space in the array (if any), and out denotes the rst full space (if any). When in == out the queue is empty. Initially, in and out are both 0.
Below are two examples of this implementation at some time during its execution. Note that when in reaches the end of the array, another insertion will make it
wrap back to the start. Therefore, in can be less than out as in the second example
The following is the start of the queue implementation in Dafny.
class BoundedQueue<T(0)>
{
// public view of the class
ghost var contents: seq<T> // the contents of the bounded queue ghost var N: nat // the (maximum) size of the bounded queue
ghost var Repr: set<object> // private implementation var data: array<T>
var in: nat
var out: nat
.. .
}
// the set of objects used in the implementation
Each part of the question is worth 4 marks.
(a) Provide an invariant for the class (encoded as usual as a Dafny predicate, Valid).
(b) Provide method signatures and specications for the methods Insert, which
inserts an element into the bounded queue, and Remove , which removes an element from the bounded queue.
Get the Solution to This Question
WeChat (微信)
WhatsApp
