Annotation Interface Impure
Impure is a method annotation that means the method might have side effects and/or might
be nondeterministic. Conceptually, it completes the "lattice" of purity annotations by serving as
a top element. That is, any @Pure method can be treated as @SideEffectFree or @Deterministic, and any @SideEffectFree or
@Deterministic method can be treated as @Impure.
This annotation should not be written by a programmer, because leaving a method unannotated is equivalent to writing this annotation.
The purpose of this annotation is for use by tools. A tool may distinguish between unannotated
methods (that the tool has not yet examined) and @Impure methods (that the tool has
determined to be neither @SideEffectFree nor @Deterministic).
- See the Checker Framework Manual:
- Side effects, determinism, purity, and
flow-sensitive analysis