CPSC 2150 - DAY 21
NOVEMBER 15, 2016

================================================================================

Exam #2 Review
--------------


1. Develop a test plan containing 3 test points (set of valid inputs/outputs)
for the queue operation.  Assume that the maximum lengths of both queues are 3

public interface MysteryOpInterface extends IntegerQueue {
/**
 * updates this, q;
 * requires |this| < maxLength and 0 < |q|;
 * ensures this = #this o PrtBtwn (0, 1, q) and 
 * 		q = PrtBtwn(1, |#q|, #q);
 */
 void mysteryOP(integerQueue q);
}

SOLUTION
--------

Inputs			|	Outputs
-----------------------------------------------------
#this	|	#q	|	this	|	q
<7,8>	|	<1,2,3>	|	<7,8,1>	|	<2,3>
<>      |	<1,2,3> |	<1>	|	<2,3>
<>	|	<1>	|	<1>	|	<>



2. 

	public interface QueueWithInject extends IntegerQueue {
	/*
	 * updates this, q;
	 * requires |this| < maxLength;
	 * ensures this = <x> o #this;
	 */
	 void inject (Integer x);
	}

	abstract class InjectOpCls implements QueueWithInject {
		@Override
		void inject (Integer x)	{
	
	SOLUTION
	--------	
	
		int len = this.length();
		this.enqueue(x);
			for (int i = 1; i <= len: i++) {
				this.enqueue(this.dequeue());
			}
		}

3.

	Suppose that Queue1 and Queue2 are two classes that implement
	QueueWithInject.  You need to show the class headers.  You don't
	need to provide any code for the methods. But you need to show what
	methods will be coded.

	a. Show how you would set up Queue1 using the abstract class
	InjectOpCls.

	b. Show how you would set up Queue2 without using the abstract class
	InjectOpCls
	
	c. What is the difference between a and b


	SOLUTION
	--------
		a. public class Queue1 extends InjectOpCls...

		b. public class Queue implements QueueWithInject...

		c. The first one is better.



4. Write the code for the constructor and dequeue, so they conform the given
invariant and correspondence.

	public class Queue3 implements IntegerQueue {
	/**
	  * invariant 0 <= front <= contents.length;
	  * correspondence conceptual this = 
	  * 	contents[front..contents.length - 1];
	  */


	SOLUTION
	--------

	Integer[] contents;
	int front;

	Queue3(int len) {
		contents = new Integer[length];
		Front = len;
	}

	Integer dequeue(Integer x)	{
		return contents[front++];
	}


5. Modify the given IntegerQueue interface so that it is a generic Queue
interface (name it IQueue) and write a generic class to implement it.  You
need to show the representaion and some plausible code for the constructor
and enqueue operations.  No need to write contracts or any other assertions.
This question says plausible code because no correspondence is given.

	SOLUTION
	--------

	Interface IQueue<T> {
		void enqueue(T x);
		T dequeue ();
		
		...
	}

	public class GenericQueue<T> implements IQueue {
		T[] contents;
		int front;

		Queue3 (int len) {
			contents = (T[]) new Object[len];
			front = len;
		}

		T dequeue() {
			return(contents[front++]_;
		}


6. What assertions need to be confirmed to prove the correctness of the
following code?

	/**
	  * requires |qi| < qi's maxLength;
	  */

	void doNothing (QueueWithInject qi) {
		Integer i;
		qi.inject(i);
		qi.dequeue();
	}

	SOLUTION
	--------

	Implicitly it says restores qi.  
	Before inject, prove |#qi| < maxLength;
	Before dequeue, prove: |<i> o #qi| > 0 
	At the end, prove qi = #qi;