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.
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.javawas introduced, which supersedes thepackage.htmldocumentation and also allows to set information for the package. For example, JSpecif allows the user to specify the nullness semantics for a complete package.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_nullnonnull\_by\_default nullable,nullable\_by\_defaultThis should be compared with the JSpecify semantics for their common nullable annotation.
@Options(...)may also be suitable.