Optional checker: implicit `@MaybePresent` annotations are inserted in `.ajava` files

Summary

An execution of WPI on a Java project with the Optional Checker will yield a set of .ajava files where the implicit @MaybePresent annotation is inserted for most (if not all) method arguments and return types, e.g.,

@org.checkerframework.dataflow.qual.Impure
public @org.checkerframework.checker.optional.qual.MaybePresent ResolvedReferenceTypeDeclaration toTypeDeclaration(@org.checkerframework.checker.optional.qual.MaybePresent JavaSymbolSolver this, @org.checkerframework.checker.optional.qual.MaybePresent Node node)

A research discussion with @mernst and @rjust showed that this was not an error; since .ajava files are not meant to be human-read.

That said, I am opening this issue to at least document the possibility that @MaybePresent annotations will no longer be inserted into the .ajava files. The manual suggests that the

[MaybePresent] type is a default value, so programmers do not have to write it

See this manual section for details.

Start with the Optional Checker manual section on annotations and review the issue discussion about implicit @MaybePresent annotations in generated .ajava files. Update the documentation to describe this behavior and clarify that .ajava files are not intended for human reading; done means the possibility is accurately documented.