Add new potential annotations and update existing ones

src/integrationTest/java/org/jspecify/nullness/NullMarkedTest.java

@@ -72,7 +72,9 @@ void assumeJava9OrLater() {
     @Test
     void annotationIncludesModuleAsTarget() {
       Set<String> targets = loadTargets();
-      assertEquals(new HashSet<String>(Arrays.asList("TYPE", "PACKAGE", "MODULE")), targets);
+      assertEquals(
+          new HashSet<String>(Arrays.asList("TYPE", "METHOD", "CONSTRUCTOR", "PACKAGE", "MODULE")),
+          targets);
     }
   }
 }

src/main/java/org/jspecify/nullness/Implies.java

@@ -0,0 +1,44 @@
+/*
+ * Copyright 2022 The JSpecify Authors.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package org.jspecify.nullness;
+
+import static java.lang.annotation.ElementType.ANNOTATION_TYPE;
+import static java.lang.annotation.RetentionPolicy.RUNTIME;
+
+import java.lang.annotation.Annotation;
+import java.lang.annotation.Documented;
+import java.lang.annotation.Repeatable;
+import java.lang.annotation.Retention;
+import java.lang.annotation.Target;
+
+/**
+ * Indicates that one annotation conveys (at least) all of the same meaning as some other
+ * annotation; for example, {@code @Implies(One.class) @interface Two {}} says that any occurrence
+ * of {@code @Two} implicitly conveys all of the meaning that {@code @One} would in that same
+ * position. Note that the {@code Two} annotation type may define additional meaning of its own as
+ * well, perhaps even adding additional usages of {@code @Implies}.
+ *
+ * <p><b>WARNING:</b> This annotation is under development, and <i>any</i> aspect of its naming,
+ * location, or design may change before 1.0. <b>Do not release libraries using this annotation at
+ * this time.</b>
+ */
+@Documented
+@Repeatable(ImpliesAnnotations.class)
+@Retention(RUNTIME)
+@Target(ANNOTATION_TYPE)
+public @interface Implies {
+  Class<? extends Annotation> value();
+}

src/main/java/org/jspecify/nullness/ImpliesAnnotations.java

@@ -0,0 +1,37 @@
+/*
+ * Copyright 2022 The JSpecify Authors.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package org.jspecify.nullness;
+
+import static java.lang.annotation.ElementType.ANNOTATION_TYPE;
+import static java.lang.annotation.RetentionPolicy.RUNTIME;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.Retention;
+import java.lang.annotation.Target;
+
+/**
+ * Container annotation for the repeatable {@link Implies @Implies} annotation.
+ *
+ * <p><b>WARNING:</b> This annotation is under development, and <i>any</i> aspect of its naming,
+ * location, or design may change before 1.0. <b>Do not release libraries using this annotation at
+ * this time.</b>
+ */
+@Documented
+@Retention(RUNTIME)
+@Target(ANNOTATION_TYPE)
+public @interface ImpliesAnnotations {
+  Implies[] value();
+}

src/main/java/org/jspecify/nullness/NonNull.java

@@ -0,0 +1,40 @@
+/*
+ * Copyright 2022 The JSpecify Authors.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package org.jspecify.nullness;
+
+import static java.lang.annotation.ElementType.TYPE_USE;
+import static java.lang.annotation.RetentionPolicy.RUNTIME;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.Retention;
+import java.lang.annotation.Target;
+
+/**
+ * Indicates that the annotated type usage is considered to exclude {@code null} as a value (used
+ * infrequently, as we typically apply {@link NullMarked @NullMarked} to some enclosing element
+ * instead).
+ *
+ * <p>For a guided introduction to JSpecify nullness annotations, please see the <a
+ * href="https://jspecify.dev/user-guide.html">user guide</a>.
+ *
+ * <p><b>WARNING:</b> This annotation is under development, and <i>any</i> aspect of its naming,
+ * location, or design may change before 1.0. <b>Do not release libraries using this annotation at
+ * this time.</b>
+ */
+@Documented
+@Target(TYPE_USE)
+@Retention(RUNTIME)
+public @interface NonNull {}

src/main/java/org/jspecify/nullness/NullMarked.java

@@ -15,6 +15,8 @@
  */
 package org.jspecify.nullness;
 
+import static java.lang.annotation.ElementType.CONSTRUCTOR;
+import static java.lang.annotation.ElementType.METHOD;
 import static java.lang.annotation.ElementType.MODULE;
 import static java.lang.annotation.ElementType.PACKAGE;
 import static java.lang.annotation.ElementType.TYPE;
@@ -25,18 +27,17 @@
 import java.lang.annotation.Target;
 
 /**
- * Indicates that within the annotated scope (class, package, or module), type usages
- * <i>generally</i> do <i>not</i> include {@code null} as a value, unless they are individually
- * marked otherwise using {@link Nullable} (or checker-specific other annotations). Without this
- * annotation, unmarked type usages would instead have <i>unspecified nullness</i>. Several
- * exceptions to this rule and an explanation of unspecified nullness are covered in the <a
- * href="http://jspecify.org/user-guide">JSpecify User Guide</a>.
+ * Indicates that the annotated element and the code transitively <a
+ * href="https://docs.oracle.com/en/java/javase/18/docs/api/java.compiler/javax/lang/model/element/Element.html#getEnclosedElements()">enclosed</a>
+ * within it is <b>null-marked code</b>: type usages are generally considered to exclude {@code
+ * null} as a value unless specified otherwise (special cases to be covered below). Using this
+ * annotation avoids the need to write {@link NonNull @NonNull} many times throughout your code.
  *
  * <p><b>WARNING:</b> This annotation is under development, and <i>any</i> aspect of its naming,
  * location, or design may change before 1.0. <b>Do not release libraries using this annotation at
  * this time.</b>
  */
 @Documented
-@Target({TYPE, PACKAGE, MODULE})
+@Target({TYPE, METHOD, CONSTRUCTOR, PACKAGE, MODULE})
 @Retention(RUNTIME)
 public @interface NullMarked {}

src/main/java/org/jspecify/nullness/NullUnmarked.java

@@ -0,0 +1,58 @@
+/*
+ * Copyright 2022 The JSpecify Authors.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package org.jspecify.nullness;
+
+import static java.lang.annotation.ElementType.CONSTRUCTOR;
+import static java.lang.annotation.ElementType.METHOD;
+import static java.lang.annotation.ElementType.MODULE;
+import static java.lang.annotation.ElementType.PACKAGE;
+import static java.lang.annotation.ElementType.TYPE;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+/**
+ * Indicates that the annotated element and the code transitively <a
+ * href="https://docs.oracle.com/en/java/javase/18/docs/api/java.compiler/javax/lang/model/element/Element.html#getEnclosedElements()">enclosed</a>
+ * within it is <b>null-unmarked code</b>: type usages generally have <b>unspecified nullness</b>
+ * unless explicitly annotated otherwise.
+ *
+ * <h2>Null-marked and null-unmarked code</h2>
+ *
+ * {@link NullMarked @NullMarked} and this annotation work as a pair to include and exclude sections
+ * of code from null-marked status. All code is considered either null-marked or null-unmarked
+ * (never both).
+ *
+ * <p>Code is considered null-marked if its most narrowly enclosing element annotated with either of
+ * these two annotations is annotated with {@link NullMarked @NullMarked}.
+ *
+ * <p>Otherwise it is considered null-unmarked: whether that’s because it is more narrowly enclosed
+ * by a {@code @NullUnmarked}-annotated element than by any {@link NullMarked @NullMarked}-annotated
+ * element, or because neither annotation is present on any enclosing element. There is no
+ * distinction made between these cases.
+ *
+ * <p><b>WARNING:</b> This annotation is under development, and <i>any</i> aspect of its naming,
+ * location, or design may change before 1.0. <b>Do not release libraries using this annotation at
+ * this time.</b>
+ *
+ * @see NullMarked {@code @NullMarked} for more information.
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({TYPE, METHOD, CONSTRUCTOR, MODULE, PACKAGE})
+public @interface NullUnmarked {}

src/main/java/org/jspecify/nullness/Nullable.java

@@ -23,10 +23,20 @@
 import java.lang.annotation.Target;
 
 /**
- * Indicates that the annotated type usage includes {@code null} as a value. To understand the
- * nullness of <i>unannotated</i> type usages, check for {@link NullMarked} on the enclosing class,
- * package, or module. See the <a href="http://jspecify.org/user-guide">JSpecify User Guide</a> for
- * details.
+ * Indicates that the annotated type usage is considered to include {@code null} as a value. A "type
+ * usage" is commonly a variable type or method return type; other cases are covered below as well.
+ *
+ * <p>Example usages:
+ *
+ * <ul>
+ *   <li>{@code @Nullable String field;}
+ *   <li>{@code @Nullable String getField() { return field; }}
+ *   <li>void setField(@Nullable String value) { field = value; }}
+ *   <li>{@code List<@Nullable String> getList() { ... }}
+ * </ul>
+ *
+ * <p>For a guided introduction to JSpecify nullness annotations, please see the <a
+ * href="https://jspecify.dev/user-guide.html">user guide</a>.
  *
  * <p><b>WARNING:</b> This annotation is under development, and <i>any</i> aspect of its naming,
  * location, or design may change before 1.0. <b>Do not release libraries using this annotation at