Source code: edu/ucsb/ccs/jcontractor/jContractorRuntime.java
1 package edu.ucsb.ccs.jcontractor;
2
3 import java.util.*;
4
5 /**
6 * This class is used internally by jContractor, and should never
7 * be used by others.
8 *
9 * This class is used to maintain state information while contracts
10 * are checked. In particular, it keeps track of which threads are
11 * evaluating contracts so that the assertion evaluation rule can be
12 * implemented. It also provides a mechanism for storing cloned
13 * objects to check OLD references.
14 *
15 * <p>One final implementation note: jContractorRuntime is a "magic"
16 * class in the jContractor system. Because contract checking code
17 * calls the methods of this class, this class cannot have contracts
18 * of its own. If it did, then they would need code that called
19 * themselves, which wouldn't do at all. So jContractorRuntime must
20 * remain contract-less. jContractor will ignore any contracts
21 * written for this class.
22 *
23 * <p><b>Assertion Evaluation Rule</b>
24 * <p>The Assertion Evaluation Rule states that when a program is
25 * evaluating a contract, no other contracts should be evaluated.
26 * What this means is that the contracts of any methods that the first
27 * contract calls will not be evaluated.
28 *
29 * <p>For example:
30 *
31 * <pre>
32 * public class MyClass {
33 * public void foo () {
34 * return true;
35 * }
36 *
37 * protected boolean foo_Precondition () {
38 * return bar();
39 * }
40 *
41 * public boolean bar () {
42 * return true;
43 * }
44 *
45 * protected boolean bar_Precondition () {
46 * return false;
47 * }
48 * }
49 * </pre>
50 *
51 * <p>Calling the <code>foo()</code> method will <i>not</i> result in a
52 * contract violation becuase the <code>bar()</code> precondition will
53 * not be evaluated while the <code>foo()</code> precondition is under
54 * evaluation.
55 *
56 * <p>The Assertion Evaluation Rule exists to prevent recursive contract
57 * checking, and because it is hard to say what
58 * the problem is if an assertion is violated while checking another
59 * assertion (which one failed?). The assumption is that if you are
60 * calling a method from a contract, you trust that method enough that
61 * its contract doesn't need to be checked.
62 *
63 * <p>jContractor implements the Assertion Evaluation Rule by locking
64 * assertion checking when a thread starts to evaluate an assertion.
65 * This is done by calling the <code>lockAssertionCheck()</code>
66 * method. No other assertions will be evaluated until the lock has
67 * been released by <code>releaseAssertionCheck()</code>.
68 *
69 * <p><b>OLD objects</b>
70 * <p>jContactor allows postconditions to refer the state of an object
71 * at method entry calling methods on the OLD object, as in "return
72 * count == OLD.count() + 1". When execution enters a method whose
73 * postcondition refers to OLD, the object is cloned, and the clone is
74 * pushed onto a stack held this class. When the postcondition is
75 * checked, the cloned object is popped from the stack. All of this
76 * is necessary because there may be any number of method calls
77 * between method entry and the postcondition check. So OLD may be
78 * saved any number of times.
79 *
80 * @author Parker Abercrombie
81 * @version $Id: jContractorRuntime.java,v 1.4 2002/05/22 06:28:48 parkera Exp $
82 */
83
84 public class jContractorRuntime {
85
86 /**
87 * Set of Threads that are checking assertion. Further contracts
88 * should not be checked on these threads.
89 */
90 protected static HashSet threadsCheckingContracts = new HashSet();
91
92 /**
93 * A hashtable of Stacks, each of which cooresponds to the execution
94 * of a Thread. As the thread executes, it will need to save the
95 * state of objects to check OLD conditions in the postcondition.
96 * Of course, between saving state and evaluating the postcondition
97 * there may be any number of calls to other methods that need to
98 * save state, or even recursive calls requiring multiple saves. In
99 * order to keep all of these saved objects in order, they are
100 * pushed onto a stack held in this table.
101 *
102 * @see #pushState(Object)
103 * @see #popState()
104 */
105 protected static Hashtable savedStates = new Hashtable();
106
107 /**
108 * Save the state of an object for retrieval later.
109 *
110 * @param stateObject the object to save.
111 *
112 * @see #popState()
113 */
114 public static synchronized void pushState (Object stateObject) {
115 Stack s = (Stack) savedStates.get(Thread.currentThread());
116 if (s == null) {
117 s = new Stack();
118 savedStates.put(Thread.currentThread(), s);
119 }
120 s.push(stateObject);
121 }
122
123 /**
124 * Recall the last saved state for a thread of execution.
125 *
126 * @return the last state saved by thread <code>t</code>, or null if
127 * there is no saved state.
128 *
129 * @see #pushState(Object)
130 *
131 * @exception EmptyStackException if there are no saved objects on
132 * the stack.
133 */
134 public static synchronized Object popState () throws EmptyStackException {
135 Stack s = (Stack) savedStates.get(Thread.currentThread());
136 if ((s != null) && !s.empty()) {
137 return s.pop();
138 } else {
139 throw new EmptyStackException();
140 }
141 }
142
143 /**
144 * Lock assertion checking for the current thread. After doing
145 * this, <code>canCheckContract()</code> will return false until the
146 * thread is released by calling
147 * <code>releaseAssertionCheck()</code>.
148 */
149 public static synchronized void lockAssertionCheck () {
150 threadsCheckingContracts.add(Thread.currentThread());
151 }
152
153 /**
154 * Release the assertion checking lock for the current thread.
155 * After doing this, <code>canCheckContract()</code> will return
156 * true until the thread is locked again by calling
157 * <code>lockAssertionCheck()</code>.
158 */
159 public static synchronized void releaseAssertionCheck () {
160 threadsCheckingContracts.remove(Thread.currentThread());
161 }
162
163 /**
164 * Determine if the current thread can evaluate an assertion. The
165 * thread is allowed to evaluate an assertion only if it is not
166 * already evaluating one (i.e. if it has not been locked).
167 *
168 * @return true if the current thread is allowed to evaluate an
169 * assertion.
170 */
171 public static synchronized boolean canCheckAssertion () {
172 return !threadsCheckingContracts.contains(Thread.currentThread());
173 }
174
175 public static void checkpoint () {
176 Stack s = (Stack) savedStates.get(Thread.currentThread());
177 if ((s != null) && !s.empty()) {
178 System.out.println(s);
179 } else {
180 throw new EmptyStackException();
181 }
182 }
183 }