SE-2832 Introduction to Software Verification

Dr. Mark Sebern -- Spring quarter 2013-2014

Lab 1

Revised: 15 March 2014


This lab was developed by Dr. Walt Schilling; all errors in its adaptation are the responsibility of the instructor.


In this lab, you will use JUnit to test an implementation of a circular queue, correct any defects that you find, and verify correct operation of the corrected code.


One commonly used low level data structure is the circular queue or circular buffer. It is often used in systems which requires fast adds and removed, as unlike other forms of queues, additions and removals can be designed to be atomic without the usage of blocks.

For this lab, you have been provided with a full implementation for a Java circular queue class. However, this code has not been tested and will most likely contain errors. You are responsible for developing JUnit tests to ensure that this class operates properly. If there are problems with the implementation, you will need to go into the source code and perform the appropriate fixes.

It is possible that there are some methods which are not implemented in the source code. If the methods are not implemented, it is acceptable for the code to simply throw an UnsupportedOperationException.

The queue, as it is structured, is perfectly capable of holding null references. Therefore, you should make certain that a null reference can be added to the queue.

Code to be tested

The code to be tested is supplied in this ZIP file.


See the javadoc for more information on the CircularQueue class and its FixedSizeQueueInterface, and for the Java Queue interface.

Assignment submission (due by 11:59PM CDT, Monday, March 17)

Prepare a PDF report (named "SE2832-username-Lab1.pdf", where "username" is your MSOE email username) on your lab experience, including:

Put this report in the top-level directory of your project.

Submit your project (i.e., your Eclipse project tree, including your report) using git to your personal Bitbucket repository (""), committing it to branch "lab1" (not "master"); if you are not sure how to do this, you can use the "master" branch for this assignment. Note that your MSOE username and Bitbucket username may differ, but the repository path incorporates your MSOE username (even though you may need to log in to Bitbucket with a different username). DO NOT submit your bin (class files) directory tree! Use .gitignore to skip the .class files.