Annotation on Package- and Module-Level

[wadoon]

Background

I just looked into Appendix A of the current draft and recognize, that modifiers are only considered for classes, interfaces, methods, fields and variables.

Starting with Java 5, the package-info.java was introduced, which supersedes the package.html documentation and also allows to set information for the package. For example, JSpecif allows the user to specify the nullness semantics for a complete package.

@NullMarked
package com.ace;

import org.jspecify.NullMarked;

This is also valid for the module-info.java.

Proposal

We should allow some JML modifiers on the package and module. The semantics are their inheritance on all classes in the module or package. This means nearly every class-level modifier is also valid for packages.

• In detail, the following modifier seems suitable: code_bigint_math, code_java_math, code_safe_math, spec_bigint_math, spec_java_math, spec_protected, spec_public, spec_pure, spec_safe_math, strictly_pure.

• Class-level but maybe strange would be modifier model.

• Nullability would be nice to control generally, e.g., override the default of non-null by default: non_null nonnull\_by\_default nullable, nullable\_by\_default

  This should be compared with the JSpecify semantics for their common nullable annotation.

• @Options(...) may also be suitable.