package org.checkerframework.checker.initialization.qual;

import java.lang.annotation.Documented;
import java.lang.annotation.ElementType;
import java.lang.annotation.Retention;
import java.lang.annotation.RetentionPolicy;
import java.lang.annotation.Target;
import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.framework.qual.SubtypeOf;

/**
 * This type qualifier indicates that an object is (definitely) in the process of being
 * constructed/initialized. The type qualifier also indicates how much of the object has already
 * been initialized. Please see the manual for examples of how to use the annotation (the link
 * appears below).
 *
 * <p>Consider a class {@code B} that is a subtype of {@code A}. At the beginning of the constructor
 * of {@code B}, {@code this} has the type {@code @UnderInitialization(A.class)}, since all fields
 * of {@code A} have been initialized by the super-constructor. Inside the constructor body, as soon
 * as all fields of {@code B} are initialized, then the type of {@code this} changes to
 * {@code @UnderInitialization(B.class)}.
 *
 * <p>Code is allowed to store potentially not-fully-initialized objects in the fields of a
 * partially-initialized object, as long as all initialization is complete by the end of the
 * constructor.
 *
 * <p>What type qualifiers on the field are considered depends on the checker; for instance, the
 * {@link org.checkerframework.checker.nullness.NullnessChecker} considers {@link NonNull}. The
 * initialization type system is not used on its own, but in conjunction with some other type-system
 * that wants to ensure safe initialization.
 *
 * <p>When an expression has type {@code @UnderInitialization}, then no aliases that are typed
 * differently may exist.
 *
 * @checker_framework.manual #initialization-checker Initialization Checker
 * @checker_framework.manual #underinitialization-examples Examples of the @UnderInitialization
 *     annotation
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(UnknownInitialization.class)
public @interface UnderInitialization {
  /**
   * The type-frame down to which the expression (of this type) has been initialized at least
   * (inclusive). That is, an expression of type {@code @UnderInitialization(T.class)} has all
   * type-frames initialized starting at {@code Object} down to (and including) {@code T}.
   *
   * @return the type whose fields are fully initialized
   */
  Class<?> value() default Object.class;
}