The Purity Checker identifies methods that have no side effects, that return the same value each time they are called on the same argument, or both.
Purity analysis aids type refinement (Section 33.7).
All checkers utilize purity annotations on called methods. You do not need to run the Purity Checker directly. However, you may run just the Purity Checker by supplying the following command-line option to javac: -processor org.checkerframework.framework.util.PurityChecker. That
implies -AcheckPurityAnnotations, so you do not need to supply both options.
The Checker Framework can infer purity annotations. If you supply the command-line option -AsuggestPureMethods, then the Checker Framework will suggest methods that can be marked as @SideEffectFree, @Deterministic, or @Pure. In addition,
such suggestions are output by -Ainfer and when using whole-program inference.
@SideEffectFreeindicates that the method has no externally-visible side effects.
@Deterministic
indicates that if the method is called multiple times with identical arguments, then it returns the identical result according to == (not just according to equals()).
@Pure
indicates that the method is both @SideEffectFree and @Deterministic.
By default, purity annotations are trusted. Purity annotations on called methods affect type-checking of client code. However, you can make a mistake by writing @SideEffectFree on
the declaration of a method that is not side-effect-free, or by writing @Deterministic on the declaration of a method that is not deterministic.
When you run the Purity Checker directly, it checks the annotations. To enable checking of the annotations when running any other checker, supply the command-line option -AcheckPurityAnnotations. For checkers other than the Purity Checker, it is not enabled by default because of a high false
positive rate. In the future, after a new purity-checking analysis is implemented, the Checker Framework will default to checking purity annotations.
A purity annotation is inherited: if a method in a superclass or superinterface has a purity annotation, then every overriding definition has that annotation too, even if the annotation is not written on the overriding definition. An overriding definition may strengthen the specification by writing a stronger annotation, but it cannot weaken it.
For example, the Object class is annotated as:
class Object {
...
@Pure int hashCode() { ... }
}
(where @Pure means both @SideEffectFree and @Deterministic). Therefore, every definition of hashCode, including those in your program, is implicitly annotated as @Pure and its body is checked
accordingly:
MyClass.java:1465: error: [purity.assign.field] field assignment not allowed in deterministic side-effect-free method
this.hash = h;
^
You can fix the definition by making its body pure. Alternately, you can suppress the warning; see Chapter 34.
The command-line options -AassumeSideEffectFree, -AassumeDeterministic, and -AassumePure make the Checker Framework unsoundly assume that every called method is side-effect-free, is deterministic, or is both, respectively.
The command-line option -AassumePureGetters makes the Checker Framework unsoundly assume that every getter method is side-effect-free and deterministic. For the purposes of -AassumePureGetters, a getter method is defined as an instance method with no formal parameters,
whose name starts with “get”, “is”, “not”, or “has” followed by an uppercase letter.
These options can make flow-sensitive type refinement much more effective, since method calls will not cause the analysis to discard information that it has learned. However, these options can mask real errors. They are most appropriate when one of the following is true:
• You are starting out annotating a project.
• You are using the Checker Framework to find bugs but not to give a guarantee that no more errors exist of the given type.
• You are working with an unannotated library that makes the given assumptions, in which case (say) using -AassumePureGetters is easier than writing stub files for all the library’s getter methods.