checker/tests/initialization/FBCList.java

import org.checkerframework.checker.initialization.qual.NotOnlyInitialized;
import org.checkerframework.checker.initialization.qual.UnderInitialization;
import org.checkerframework.checker.nullness.qual.Nullable;

// This example is taken from the FBC paper, figure 1 (and has some additional code in main below).
// We made the list generic.
public class FBCList<T> {
  @NotOnlyInitialized FBCNode<T> sentinel;

  public FBCList() {
    this.sentinel = new FBCNode<>(this);
  }

  void insert(@Nullable T data) {
    this.sentinel.insertAfter(data);
  }

  public static void main() {
    FBCList<Integer> l = new FBCList<>();
    l.insert(1);
    l.insert(2);
  }
}

class FBCNode<T> {
  @NotOnlyInitialized FBCNode<T> prev;

  @NotOnlyInitialized FBCNode<T> next;

  @NotOnlyInitialized FBCList parent;

  @Nullable T data;

  // for sentinel construction
  FBCNode(@UnderInitialization FBCList parent) {
    this.parent = parent;
    this.prev = this;
    this.next = this;
  }

  // for data node construction
  FBCNode(FBCNode<T> prev, FBCNode<T> next, @Nullable T data) {
    this.parent = prev.parent;
    this.prev = prev;
    this.next = next;
    this.data = data;
  }

  void insertAfter(@Nullable T data) {
    FBCNode<T> n = new FBCNode<>(this, this.next, data);
    this.next.prev = n;
    this.next = n;
  }
}