CPSC 2150 - DAY 16
OCTOBER 20, 2016

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

Formal Reasoning: Top Method

	.So four items need to be proved:

		One for the implicit ensures clasue of top
		One for ensures clauses for top
		One for the requires clasue of pop
		One for the requires clause of push

Generics
--------

Generics in Java (and Templates in C++)

Users can employ same interfaces and classes in different situations by
instantiating them appropriately

Key idea: Development, testing, and verification of generic modules can happen
once in their lifetime: the cost is amortized through many uses

How to build new generic interfaces and classes and reuse them

What generic collections are avaliable in the Java library and how to reuse them

public interface IStack <T>	{
	public void push (T x);
	public T pop();
	public int depth();
	public void clear();
	public int maxDepth();
}

Note that Istack is a generic type (also called a parameterized type)

The actual type of entries is selected only later by the client when type
Istack is used to declare or instantiate a variable

Istack<Integer> si = new Stack1<Integer>(10);

Note that use of Integer here, not int

Java demands that generic arguments must be reference types

Each of the primitive types has a corresponding wrapper type, that is a 
reference type

***aliases reference x***  this means that an alias is copied onto the stack

The tracing table notation with -> gives us no easy way to describe this 
situation

copy vs. clone