证明迭代键的 `get` 非空

Question

我有一个具有类似地图功能的界面，但没有实现 Java 的地图界面。
地图接口也实现了Iterable<Object>；它遍历地图的键
我想在增强循环的主体中使用 this（见下文），但没有断言，并使用 get 来检索迭代键的值，并且没有来自 Checker Framework 的 [ERROR]。
这完全有可能吗？您能否提供从哪里开始的指示或可供学习的示例？我尝试随意地在这里和那里洒一些 @KeyFors，但是由于缺乏完全理解我在做什么，我可能需要一段时间才能找到正确的位置 ;-)
我知道我们可能会使用 "Entry Iterator" 并避免首先解决这个问题，但我真的只是想学习如何教 Checker Framework 关于 a 之间的语义关系键迭代器和一个 @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 可能 return 随时为空，客户端无法知道 return 值何时可能为非空：

   @Nullable Object get(Object o);

如果你想声明一个方法的 return 值在一般情况下是可以为空的，但在某些情况下是非空的，那么你需要使用 条件后置条件 例如@EnsuresNonNullIf.

也就是说，Nullness Checker 有 special handling for Map.get。您的代码不使用它，因为您没有覆盖 java.util.Map.get 的方法（尽管它确实有一个名为 Map 的 class 与 java.util.Map).

如果您想要 IMap.get 的特殊情况处理，则：

您的 class 应该扩展 java.util.Map，或者
您应该扩展 Nullness Checker 以识别您的 class。

地图键问题

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

我建议从 Checker Framework Manual. It has lots of explanations and examples. You should read at least the Map Key Checker chapter. It links to further documentation, such as 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; instead, think first and 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() {

这些注释状态，分别为：

此对象的迭代器 returns 键。
客户端必须为此对象传递密钥。
此对象的迭代器 returns 键。我抑制了警告，因为此对象充当包含对象的包装器，我不记得 Checker Framework 有一种说法，"This object is a wrapper around a field and each of its methods has the same properties as the methods of that field."

结果类型检查没有问题（除了本答案第一部分中指出的无效）：

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 的特殊情况。

证明迭代键的 `get` 非空

Prove non-nullness of `get` for iterated keys

java

checker-framework

空性问题

地图键问题