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

2 回答 2

2

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 来识别你的类。

地图键问题

你能提供从哪里开始的指导或学习的例子吗？

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

我随意尝试在这里和那里撒一些@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. 迭代器返回此对象的键。我取消了警告，因为该对象充当包含对象的包装器，而且我不记得检查器框架有办法说：“此对象是字段的包装器，它的每个方法都具有相同的属性作为那个领域的方法。”

结果类型检查没有问题（除了这个答案第一部分中提到的空值）：

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();
    }
}
于 2019-08-14T17:05:31.393 回答
0

总结信息丰富的接受答案：

  1. 没有办法注释给定的代码示例，以便可以将迭代器和 IMap 的 get 方法之间的语义关系指定给 Checker Framework；
  2. 因此，当前报告的错误需要本地非空性断言，重写代码以避免键迭代器或 SuppressWarning 注释。
  3. 如果我们想避免这些变通办法，就需要对检查器框架进行扩展，其中包括它是如何为 java.util.Map 提供特殊情况的。
于 2019-08-16T18:34:08.060 回答