Question 5 [10 marks]
A bounded, ordered queue is a queue with maximum length, max, whose elements are returned in order from largest to smallest (irrespective of the order they were placed in the queue).
The following ghost and non-ghost variables represent the abstract and concrete states, respectively, of a Dafny class implementing a bounded, ordered queue whose elements are integers.
ghost var elems: seq<int>; ghost var max: nat;
ghost var Repr: set<object>; var a: array<int>;
// the elements in the queue
// the maximum size of the queue
// the set of objects implementing the queue // an array storing the elements of the queue // the current size of the queue
var n: nat;
(a) Define a class invariant, Valid, constraining and relating the above variables. (6 marks)
(b) Specify a method of the class, GetValue, which returns the next element from the queue. (4 marks)
