1
2
3
4
5
6
7
8
9
10
11
12
13
14 package net.sf.jgabl2.core.util.check;
15
16
17 /**
18 * Traits for checking of invariants and conditions. To be used by non-trivial
19 * data structures and algorithms.
20 *
21 * <p>
22 * <b>Sample: </b>
23 * </p>
24 *
25 * <p>
26 * <pre>
27 *
28 * public class CheckingStack {
29 * CheckPolicy checkPolicy;
30 * Object[] stack;
31 * int last = -1;
32 *
33 * <b>protected void checkInvariant()
34 * throws InvariantViolatedException {
35 *
36 * }</b>
37 *
38 * public CheckingStack ( int capacity, CheckPolicy checkPolicy ) {
39 * this.checkPolicy = checkPolicy;
40 * stack = new Object[capacity];
41 *
42 * if (checkPolicy.checkInvariant())
43 * checkInvariant();
44 * }
45 *
46 *
47 * public void pop() {<b>
48 * if (checkPolicy.checkPostcond() && isEmpty())
49 * throw new PrecondFailedException(
50 * "!isEmpty()");</b>
51 *
52 * --last;
53 * }
54 *
55 * // unchecked version
56 * public Object _top() {
57 * return stack[last];
58 * }
59 *
60 * public Object top() {
61 * <b>if (checkPolicy.checkPostcond() && isEmpty())
62 * throw new PrecondFailedException(
63 * "!isEmpty()");</b>
64 *
65 * return stack[last];
66 * }
67 *
68 * public void push ( Object value ) {
69 * <b>if (checkPolicy.checkPrecond())
70 * if (!(last < stack.length-1))
71 * throw new PrecondFailedException(
72 * "last < stack.length-1");
73 *
74 * if (checkPolicy.checkInvariantPedantic())
75 * checkInvariant();</b>
76 *
77 * stack[++last] = value;
78 *
79 * <b>if (checkPolicy.checkInvariant())
80 * checkInvariant();
81 *
82 * if (checkPolicy.checkPostcond()) {
83 * if (isEmpty())
84 * throw new PostcondFailedException("!isEmpty()");
85 * if (_top() != value) // using uncheck version !
86 * throw new PostcondFailedException(
87 * "top() == value");
88 * }</b>
89 *
90 * }
91 *
92 *
93 *
94 * }
95 *
96 * </pre>
97 * </p>
98 *
99 * @author Alexander Schwartz
100 * @since 0.1.0
101 */
102 public interface CheckPolicy {
103 /**
104 * Answers whether to check a precondition of a method.
105 *
106 * @return <code>true</code> if and only if
107 * the precondition should be checked.
108 */
109 public boolean checkPrecond();
110
111 /**
112 * Answers whether to check a postcondition of a method.
113 *
114 * @return <code>true</code> if andd only if
115 * the postcondition should be checked.
116 */
117 public boolean checkPostcond();
118
119 /**
120 * Answers whether to check an assumption in a method.
121 *
122 * @return <code>true</code> if and only if
123 * the assumption should be checked.
124 */
125 public boolean checkAssumption();
126
127 /**
128 * Answers whether to check of a loop invariant of a method.
129 *
130 * @return <code>true</code> if and only if
131 * the loop invariant should be checked.
132 */
133 public boolean checkLoopInvariant();
134
135 /**
136 * Answers whether to perfom an invariant check of a class.
137 * @param invariantType the type of the invariant
138 * @return <code>true</code> if and only if
139 * the invariant should be checked.
140 */
141 public boolean checkInvariant(InvariantType invariantType);
142 }