1 |
package com.instantiations.example.stack; |
2 |
|
3 |
import java.util.EmptyStackException; |
4 |
|
5 |
/** |
6 |
* The class <code>DBCStack</code> is a simple implementation of a stack that |
7 |
* contains design-by-contract (DBC) information. Other than the presence of |
8 |
* the DBC tags, this class is identical to the class {@link SimpleStack} so |
9 |
* that the results of generating test classes can be compared. |
10 |
* |
11 |
* @author Chris Cummings |
12 |
* |
13 |
* @inv top >= 0 && top <= elements.length |
14 |
*/ |
15 |
public class DBCStack |
16 |
{ |
17 |
private Object[] elements; |
18 |
|
19 |
private int top; |
20 |
|
21 |
/** |
22 |
* @pre initialCapacity > 0 |
23 |
* @post elements != null && elements.length == initialCapacity && top == 0 |
24 |
*/ |
25 |
public DBCStack(int initialCapacity) |
26 |
{ |
27 |
elements = new Object[initialCapacity]; |
28 |
} |
29 |
|
30 |
/** |
31 |
* @post $ret == (top == 0) |
32 |
*/ |
33 |
public boolean isEmpty() |
34 |
{ |
35 |
return top == 0; |
36 |
} |
37 |
|
38 |
/** |
39 |
* @post (top == $pre(int, top) + 1) && elements[top - 1] == object |
40 |
*/ |
41 |
public void push(Object object) |
42 |
{ |
43 |
if (top == elements.length) { |
44 |
grow(); |
45 |
} |
46 |
elements[top++] = object; |
47 |
} |
48 |
|
49 |
/** |
50 |
* @pre !isEmpty() |
51 |
* @post $ret == elements[top - 1] |
52 |
*/ |
53 |
public Object peek() |
54 |
{ |
55 |
if (top == 0) { |
56 |
throw new EmptyStackException(); |
57 |
} |
58 |
return elements[top - 1]; |
59 |
} |
60 |
|
61 |
/** |
62 |
* @pre !isEmpty() |
63 |
* @post (top == $pre(int, top) - 1) && $ret == elements[top] |
64 |
*/ |
65 |
public Object pop() |
66 |
{ |
67 |
if (top == 0) { |
68 |
throw new EmptyStackException(); |
69 |
} |
70 |
return elements[--top]; |
71 |
} |
72 |
|
73 |
private void grow() |
74 |
{ |
75 |
int elementCount; |
76 |
Object[] newElements; |
77 |
|
78 |
elementCount = elements.length; |
79 |
newElements = new Object[elementCount + 10]; |
80 |
System.arraycopy(elements, 0, newElements, 0, elementCount); |
81 |
elements = newElements; |
82 |
} |
83 |
} |