\CodePro Analytix Evaluation\src\com\instantiations\example\stack\DBCStack.java
Violations: 0 high, 18 medium, 3 low
 
Violations
Missing file comment Missing @return tag for isEmpty Constant on right side of comparison
Missing @version tag for type DBCStack Constant on right side of comparison Missing Javadoc comment for method "grow"
toString() is missing Missing @param tag for object in push Local variable not initialized: elementCount
Missing default constructor Nested assignment Local variable should be final: elementCount
Missing Javadoc comment for field Missing @return tag for peek Local variable not initialized: newElements
Missing Javadoc comment for field Constant on right side of comparison Local variable should be final: newElements
Missing @param tag for initialCapacity in DBCStack Missing @return tag for pop Invalid numeric literal: 10
 
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