1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
|
package org.checkerframework.dataflow.qual;
import java.lang.annotation.Documented;
import java.lang.annotation.ElementType;
import java.lang.annotation.Retention;
import java.lang.annotation.RetentionPolicy;
import java.lang.annotation.Target;
/**
* A method is called <em>deterministic</em> if it returns the same value
* (according to <tt>==</tt>) every time it is called with the same
* parameters and in the same environment. The parameters include the
* receiver, and the environment includes all of the Java heap (that is,
* all fields of all objects and all static variables).
* <p>
* This annotation is important to pluggable type-checking because, after a
* call to a <tt>@Deterministic</tt> method, flow-sensitive type refinement
* can assume that anything learned about the first invocation is true
* about subsequent invocations (so long as no non-<tt>@</tt>{@link
* SideEffectFree} method call intervenes). For example,
* the following code never suffers a null pointer
* exception, so the Nullness Checker need not issue a warning:
* <pre><code> if (x.myDeterministicMethod() != null) {
x.myDeterministicMethod().hashCode();
}</code></pre>
* <p>
* Note that <tt>@Deterministic</tt> guarantees that the result is
* identical according to <tt>==</tt>, <b>not</b> equal according to
* <tt>equals</tt>. This means that writing <tt>@Deterministic</tt> on a
* method that returns a reference is often erroneous unless the
* returned value is cached or interned.
* <p>
* Also see {@link Pure}, which means both deterministic and {@link
* SideEffectFree}.
* <p>
* <b>Analysis:</b>
* The Checker Framework performs a conservative analysis to verify a
* <tt>@Deterministic</tt> annotation. The Checker Framework issues a
* warning if the method uses any of the following Java constructs:
* <ol>
* <li>Assignment to any expression, except for local variables (and method
* parameters).
* <li>A method invocation of a method that is not {@link Deterministic}.
* <li>Construction of a new object.
* <li>Catching any exceptions. This is to prevent a method to get a hold of
* newly created objects and using these objects (or some property thereof)
* to change their return value. For instance, the following method must be
* forbidden.
* <pre>
<code>
@Deterministic
int f() {
try {
int b = 0;
int a = 1/b;
} catch (Throwable t) {
return t.hashCode();
}
return 0;
}
</code>
</pre>
* </ol>
* A constructor can be <tt>@Pure</tt>, but a constructor <em>invocation</em> is
* not deterministic since it returns a different new object each time.
* TODO: Side-effect-free constructors could be allowed to set their own fields.
* <p>
*
* Note that the rules for checking currently imply that every {@code
* Deterministic} method is also {@link SideEffectFree}. This might change
* in the future; in general, a deterministic method does not need to be
* side-effect-free.
* <p>
*
* These rules are conservative: any code that passes the checks is
* deterministic, but the Checker Framework may issue false positive
* warnings, for code that uses one of the forbidden constructs but is
* deterministic nonetheless.
* <p>
*
* In fact, the rules are so conservative that checking is currently
* disabled by default, but can be enabled via the
* <tt>-AcheckPurityAnnotations</tt> command-line option.
* <p>
*
* @checker_framework.manual #type-refinement-purity Side effects, determinism, purity, and flow-sensitive analysis
*
* @author Stefan Heule
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ ElementType.METHOD, ElementType.CONSTRUCTOR })
public @interface Deterministic {
}
|
