java - 证明迭代键的 `get` 非空

Question

• 我有一个具有类似 map 功能的接口(interface)，但没有实现 Java 的 Map 接口(interface)。
• map 接口(interface)还实现 Iterable<Object> ;它迭代 map 的键
• 我想使用this在增强循环的主体中(见下文)，但没有断言，并使用 get检索迭代键的值，并且没有 [ERROR]来自检查器框架。
• 这有可能吗？您能否提供从哪里开始的指导或可供学习的示例？我尝试随意撒一些@KeyFor到处都有，但由于缺乏完全理解我在做什么，我可能需要一段时间才能找到正确的位置;-)
• 我知道我们可能会使用“条目迭代器”并避免首先解决这个问题，但我真的只是有兴趣学习如何向 Checker 框架教授关键迭代器和一个@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

空值检查器警告您规范(类型注释)与代码本身不一致。

空值问题

您的代码的关键问题在这里:

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) { ... }

get 可能随时返回 null，而客户端无法知道返回值何时可能为非 null:

   @Nullable Object get(Object o);

如果您想声明方法的返回值一般情况下可为空，但在某些情况下为非空，则需要使用条件后置条件，例如 @EnsuresNonNullIf .

也就是说，空值检查器有 special handling for Map.get 。您的代码没有使用它，因为您没有重写 java.util.Map.get 的方法(尽管它确实有一个名为 Map 的类，该类具有与 java.util.Map 无关)。

如果您想要对 IMap.get 进行特殊情况处理，则可以:

• 您的类应该扩展java.util.Map，或者
• 您应该扩展 Nullness Checker 来识别您的类。

map 按键问题

could you provide pointers where to start or examples to learn from?

我建议从 Checker Framework Manual 开始。它有很多解释和例子。您至少应该阅读Map Key Checker chapter 。它链接到更多文档，例如 Javadoc for @KeyFor .

I tried haphazardly to sprinkle some @KeyFors here and there, but with a lack of fully understanding what I'm doing it could take a while before I hit the right spots ;-)

请不要这样做!那就是痛苦。手册tells you not to do that ;相反，首先思考 write specifications描述您的代码。

以下是您可以编写的三个 @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. 客户端必须传递该对象的 key 。
3. 迭代器返回该对象的键。我抑制了警告，因为该对象充当所包含对象的包装器，并且我不记得 Checker 框架有办法说:“该对象是字段周围的包装器，并且它的每个方法都具有相同的属性作为该领域的方法。”

结果类型检查没有问题(除了本答案第一部分中指出的空值):

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();
    }
}