@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.