证明迭代键的 `get` 非空

Question

• 我有一个具有类似地图功能的接口，但没有实现 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();

   }

}

Answer 1

Nullness Checker 警告您规范（类型注释）与代码本身不一致。无效性问题您的代码的关键问题在这里：tmp.put(k, get(k))错误信息是：error: [argument.type.incompatible] incompatible types in argument.               tmp.put(k, get(k)); // get(k) is always non-null because of the key iterator                             ^  found   : @Initialized @Nullable Object  required: @Initialized @NonNull Object以下是两个不兼容的规范：put需要一个非空的第二个参数（回想一下这@NonNull是默认值）：   public IMap put(Object key, Object value) { ... }get可能随时返回 null，而客户端无法知道返回值何时可能为非 null：   @Nullable Object get(Object o);如果你想声明一个方法的返回值在一般情况下是可以为空的，但在某些情况下是非空的，那么你需要使用条件后置条件，比如@EnsuresNonNullIf.也就是说，Nullness Checker对Map.get. 您的代码不使用它，因为您没有覆盖的方法java.util.Map.get（尽管它确实有一个名为的类Map，与 无关java.util.Map）。如果您想要对 进行特殊情况处理IMap.get，则可以：你的课程应该扩展java.util.Map，或者您应该扩展 Nullness Checker 以识别您的班级。地图关键问题你能提供从哪里开始的指导或可以学习的例子吗？我尝试随意地在这里和那里洒一些@KeyFors，但由于缺乏完全理解我在做什么，我可能需要一段时间才能找到正确的位置；-)请不要那样做！那就是痛苦。手册告诉你不要那样做；相反，首先思考并编写描述代码的规范。@KeyFor以下是您可以编写的三个注释：interface IMap extends Iterable<@KeyFor("this") Object> {...    default IMap remove(@KeyFor("this") Object key) {...    @SuppressWarnings("keyfor") // a key for `contents` is a key for this object    public java.util.Iterator<@KeyFor("this") Object> iterator() {这些注释分别说明：迭代器返回此对象的键。客户端必须为此对象传递一个密钥。迭代器返回此对象的键。我抑制了警告，因为此对象充当包含对象的包装器，而且我不记得 Checker Framework 有一种方式说“此对象是一个字段的包装器，它的每个方法都具有相同的属性作为那个领域的方法。”结果类型检查没有问题（此答案第一部分中指出的无效性除外）：import org.checkerframework.checker.nullness.qual.KeyFor;import org.checkerframework.checker.nullness.qual.NonNull;import org.checkerframework.checker.nullness.qual.Nullable;interface IMap extends Iterable<@KeyFor("this") Object> {    @Nullable Object get(Object o);    IMap put(Object key, Object value); // immutable put    IMap empty();    default IMap remove(@KeyFor("this") 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    @SuppressWarnings("keyfor") // a key for `contents` is a key for this object    public java.util.Iterator<@KeyFor("this") Object> iterator() {        return contents.keySet().iterator();    }}

Answer 2

总结信息性接受的答案：无法对给定的代码示例进行注解，使得迭代器和 IMap 的 get 方法之间的语义关系可以指定给 Checker Framework；因此，当前报告的错误需要本地非空断言，重写代码以避免键迭代器或 SuppressWarning 注释。如果我们想避免这些变通方法，那么有必要对检查器框架进行扩展，例如它是如何针对 java.util.Map 进行特殊处理的。