证明迭代键的 `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

以下是两个不兼容的规范：

1. put需要一个非空的第二个参数（回想一下这@NonNull是默认值）：

   public IMap put(Object key, Object value) { ... }

1. 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() {

这些注释分别说明：

1. 迭代器返回此对象的键。

2. 客户端必须为此对象传递一个密钥。

3. 迭代器返回此对象的键。我抑制了警告，因为此对象充当包含对象的包装器，而且我不记得 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

总结信息性接受的答案：

1. 无法对给定的代码示例进行注解，使得迭代器和 IMap 的 get 方法之间的语义关系可以指定给 Checker Framework；

2. 因此，当前报告的错误需要本地非空断言，重写代码以避免键迭代器或 SuppressWarning 注释。

3. 如果我们想避免这些变通方法，那么有必要对检查器框架进行扩展，例如它是如何针对 java.util.Map 进行特殊处理的。