/CodePro Analytix Evaluation/src/com/instantiations/example/stack/DBCStack.java
 
Code Coverage Summary 100.0% coverage
Executable Lines 19
Line Coverage 100.0%
Block Coverage 100.0%
Instruction Coverage 100.0%
    
Legend
Line is fully covered
Line is partially covered
Line is not covered
Source
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 }
Powered by CodePro AnalytiX