1. Homepage
  2. Exam
  3. CSSE3100/7100 Reasoning About Programs - Semester One 2020- Final Exam - Q7 Bounded Queue

CSSE3100/7100 Reasoning About Programs - Semester One 2020- Final Exam - Q7 Bounded Queue

This question has been solved
Engage in a Conversation

QUESTION 7 CourseNana.COM

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

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

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

wrap back to the start. Therefore, in can be less than out as in the second example CourseNana.COM


CourseNana.COM

The following is the start of the queue implementation in Dafny. CourseNana.COM

class BoundedQueue<T(0)> CourseNana.COM

{
// 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
CourseNana.COM

ghost var Repr: set<object> // private implementation var data: array<T>
var in: nat
CourseNana.COM

var out: nat CourseNana.COM

.. . CourseNana.COM

} CourseNana.COM

// the set of objects used in the implementation CourseNana.COM

Each part of the question is worth 4 marks.
(a) Provide an invariant for the class (encoded as usual as a Dafny predicate, Valid).
CourseNana.COM

(b) Provide method signatures and specications for the methods Insert, which CourseNana.COM

inserts an element into the bounded queue, and Remove , which removes an element from the bounded queue. CourseNana.COM


CourseNana.COM



CourseNana.COM

Get the Solution to This Question

WeChat WeChat
Whatsapp WhatsApp
CSSE3100代写,CSSE7100代写,Reasoning About Programs代写,Weakest Precondition Proof代写,Queensland代写,CSSE3100代编,CSSE7100代编,Reasoning About Programs代编,Weakest Precondition Proof代编,Queensland代编,CSSE3100代考,CSSE7100代考,Reasoning About Programs代考,Weakest Precondition Proof代考,Queensland代考,CSSE3100help,CSSE7100help,Reasoning About Programshelp,Weakest Precondition Proofhelp,Queenslandhelp,CSSE3100作业代写,CSSE7100作业代写,Reasoning About Programs作业代写,Weakest Precondition Proof作业代写,Queensland作业代写,CSSE3100编程代写,CSSE7100编程代写,Reasoning About Programs编程代写,Weakest Precondition Proof编程代写,Queensland编程代写,CSSE3100programming help,CSSE7100programming help,Reasoning About Programsprogramming help,Weakest Precondition Proofprogramming help,Queenslandprogramming help,CSSE3100assignment help,CSSE7100assignment help,Reasoning About Programsassignment help,Weakest Precondition Proofassignment help,Queenslandassignment help,CSSE3100solution,CSSE7100solution,Reasoning About Programssolution,Weakest Precondition Proofsolution,Queenslandsolution,