我有一個具有類似地圖功能的接口，但沒有實現 Java 的 Map 接口。地圖接口還實現了Iterable<Object>；它遍歷地圖的鍵我想this在增強循環的主體中使用（見下文），但沒有斷言，并用于get檢索迭代鍵的值，并且沒有[ERROR]來自 Checker Framework 的 an 。這完全有可能嗎？您能否提供從哪里開始的指示或可以學習的示例？我試著隨意地在這里和那里灑一些@KeyFors，但是由于缺乏完全理解我在做什么，我可能需要一段時間才能找到正確的位置；-)我知道我們可能會使用“條目迭代器”并避免首先解決這個問題，但我真的只是想學習如何向 Checker Framework 傳授鍵迭代器和方法之間的語義關系@Nullable get。這是一個最小的工作示例：import org.checkerframework.checker.nullness.qual.Nullable;interface IMap extends Iterable<Object> {    @Nullable Object get(Object o);    IMap put(Object key, Object value); // immutable put    IMap empty();    default IMap remove(Object key) {       IMap tmp = empty();       for (Object k : this) {           if (!k.equals(key)) {               tmp.put(k, get(k)); // get(k) is always non-null because of the key iterator           }       }       return tmp;    }}class Map implements IMap {   java.util.Map<Object, Object> contents = new java.util.HashMap<>();   public Map() { }   private Map(java.util.Map<Object, Object> contents) {      this.contents = contents;      }   @Override   public @Nullable Object get(Object key) {     return contents.get(key);   }   @Override   public IMap empty() {       return new Map();   }   @Override   public IMap put(Object key, Object value) {      java.util.Map<Object, Object> newContents = new java.util.HashMap<>();      newContents.putAll(contents);      newContents.put(key, value);      return new Map(newContents);   }   @Override   public java.util.Iterator<Object> iterator() {      return contents.keySet().iterator();   }}