Annotation Type 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.
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:
- Assignment to any expression, except for local variables and method parameters.
(Note that storing into an array element, such a
a[i] = x, is not an assignment to a variable and is therefore forbidden.)
- A method invocation of a method that is not
- Construction of a new object where the constructor is not
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
- See the Checker Framework Manual:
- Side effects, determinism, purity, and