@Documented @Retention(value=RUNTIME) @Target(value={METHOD,CONSTRUCTOR}) public @interface SideEffectFree
Only the visible side-effects are important. The method is allowed to cache the answer to a computationally expensive query, for instance. It is also allowed to modify newly-created objects, and a constructor is side-effect-free if it does not modify any objects that existed before it was called.
This annotation is important to pluggable type-checking because if some
fact about an object is known before a call to such a method, then the
fact is still known afterwards, even if the fact is about some non-final
field. When any non-@SideEffectFree
method is called, then a
pluggable type-checker must assume that any field of any accessible
object might have been modified, which annuls the effect of
flow-sensitive type refinement and prevents the pluggable type-checker
from making conclusions that are obvious to a programmer.
Also see Pure
, which means both side-effect-free and Deterministic
.
Analysis:
The Checker Framework performs a conservative analysis to verify a
@SideEffectFree
annotation.
The Checker Framework issues a warning
if the method uses any of the following Java constructs:
@SideEffectFree
.
@SideEffectFree
.
In fact, the rules are so conservative that checking is currently
disabled by default, but can be enabled via the
-AcheckPurityAnnotations
command-line option.