Annotation Interface Deterministic
==
)
every time it is called with the same arguments and in the same environment. The arguments
include the receiver, and the environment includes all of the Java heap (that is, all fields of
all objects and all static variables).
Determinism refers to the return value during a non-exceptional execution. If a method throws an exception, the Throwable does not have to be exactly the same object on each invocation (and generally should not be, to capture the correct stack trace).
This annotation is important to pluggable type-checking because, after a call to a
@Deterministic
method, flow-sensitive type refinement can assume that anything learned
about the first invocation is true about subsequent invocations (so long as no
non-@
SideEffectFree
method call intervenes). For example, the following code
never suffers a null pointer exception, so the Nullness Checker need not issue a warning:
if (x.myDeterministicMethod() != null) {
x.myDeterministicMethod().hashCode();
}
Note that @Deterministic
guarantees that the result is identical according to
==
, not just equal according to equals()
. This means that writing
@Deterministic
on a method that returns a reference (including a String) is often
erroneous unless the returned value is cached or interned.
Also see Pure
, which means both deterministic and SideEffectFree
.
Analysis: The Checker Framework performs a conservative analysis to verify a
@Deterministic
annotation. The Checker Framework issues a warning if the method uses any
of the following Java constructs:
- Assignment to any expression, except for local variables and method parameters.
(Note that storing into an array element, such aa[i] = x
, is not an assignment to a variable and is therefore forbidden.) - A method invocation of a method that is not
Deterministic
. - Construction of a new object.
- Catching any exceptions. This restriction prevents a method from obtaining a reference to a
newly-created exception object and using these objects (or some property thereof) to change
the method's return value. For instance, the following method must be forbidden.
@Deterministic int f() { try { int b = 0; int a = 1/b; } catch (Throwable t) { return t.hashCode(); } return 0; }
Deterministic
(or @Pure
), that means that all
the fields are deterministic (the same values, if the arguments are the same). The constructed
object itself is different. That is, a constructor invocation is never deterministic
since it returns a different new object each time.
Note that the rules for checking currently imply that every Deterministic
method is
also SideEffectFree
. This might change in the future; in general, a deterministic method
does not need to be side-effect-free.
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.
In fact, the rules are so conservative that checking is currently disabled by default, but can
be enabled via the -AcheckPurityAnnotations
command-line option.
This annotation is inherited by subtypes, just as if it were meta-annotated with
@InheritedAnnotation
.
- See the Checker Framework Manual:
- Side effects, determinism, purity, and
flow-sensitive analysis