org.checkerframework.dataflow.qual

Annotation Type SideEffectFree

@Documented
 @Retention(value=RUNTIME)
 @Target(value={METHOD,CONSTRUCTOR})
public @interface SideEffectFree

A method is called side-effect-free if it has no visible side-effects, such as setting a field of an object that existed before the method was called.

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:

1. 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.)
2. A method invocation of a method that is not @SideEffectFree.
3. Construction of a new object where the constructor is not @SideEffectFree.

These rules are conservative: any code that passes the checks is side-effect-free, but the Checker Framework may issue false positive warnings, for code that uses one of the forbidden constructs but is side-effect-free nonetheless. In particular, a method that caches its result will be rejected.

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