Resizing Arrays

A weakness of this implementation is that it chooses an arbitrary size for the array when the Stack is created. If the user pushes more than 128 items onto the stack, it will cause an ArrayIndexOutOfBounds exception.

An alternative is to let the client code specify the size of the array. This alleviates the problem, but it requires the client to know ahead of time how many items are needed, and that is not always possible.

A better solution is to check whether the array is full and make it bigger when necessary. Since we have no idea how big the array needs to be, it is a reasonable strategy to start with a small size and double it each time it overflows.

Here's the improved version of push:

Before putting the new item in the array, we check if the array is full. If so, we invoke resize. After the if statement, we know that either (1) there was room in the array, or (2) the array has been resized and there is room. If full and resize are correct, then we can prove that index < array.length, and therefore the next statement cannot cause an exception.

Now all we have to do is implement full and resize.

Both methods are declared private, which means that they cannot be invoked from another class, only from within this one. This is acceptable, since there is no reason for client code to use these functions, and desirable, since it enforces the boundary between the implementation and the client.

The implementation of full is trivial; it just checks whether the index has gone beyond the range of valid indices.

The implementation of resize is straightforward, with the caveat that it assumes that the old array is full. In other words, that assumption is a precondition of this method. It is easy to see that this precondition is satisfied, since the only way resize is invoked is if full returns true, which can only happen if index == array.length.

At the end of resize, we replace the old array with the new one (causing the old to be garbage collected). The new array.length is twice as big as the old, and index hasn't changed, so now it must be true that index < array.length. This assertion is a postcondition of resize: something that must be true when the method is complete (as long as its preconditions were satisfied).

Preconditions, postconditions, and invariants are useful tools for analyzing programs and demonstrating their correctness. In this example I have demonstrated a programming style that facilitates program analysis and a style of documentation that helps demonstrate correctness.