@EnsuresNonNullIf 注释给出“条件后置条件不满足”-警告

Question

我正在使用检查器框架和类型注释来检查@Nullable 和@NonNull 的正确使用。 在类似 Map 的类¹ 中，Java 规范声明当映射不包含该键的条目时，get(…)-methods 返回 null。因此，这些方法具有@Nullable-注解。但是，当contains(…) 返回true 时，我想保证get(…) 不会返回null。

如何指定条件 NonNull？

据我所知，您可以通过使用@EnsuresNonNullIf 注释contains(…)-方法来实现这一点，如下所示：

@Pure
@EnsuresNonNullIf(expression = {"get(#1)", "getMatchingStoredKey(#1)", "getStrict(#1)", "lookup(#1)"}, result = true)
public boolean containsKeyStrict(final @Nullable Class<? extends TKeyClass> key) {
    return super.containsKey(key);
}

@Pure
public @Nullable TValue getStrict(final @Nullable Class<? extends TKeyClass> key) {
    Return super. gets (key);
}

但是，这会导致警告：

the conditional postcondition about 'this.getStrict(key)' at this return statement is not satisfied

我应该如何解决这个“后置条件不满足”的警告？

我的环境：

• Maven：3.0.4
• Java：1.7.0_25（甲骨文）
• Checker 框架 1.7.0（通过 maven 插件）

This Gist 演示了这个问题。

---

1) 它扩展了地图的功能，以检索具有“相似”键的条目。

Answer 1

到目前为止，我唯一的解决方案是将@EnsuresNonNullIf-annotation 与SuppersWarnings("nullness") 结合使用。例如：

@SuppressWarnings("nullness")
@EnsuresNonNullIf(expression = {"get(#1)", "getMatchingStoredKey(#1)", "getStrict(#1)", "lookup(#1)"}, result = true)
public boolean containsKeyStrict(final @Nullable Class<? extends TKeyClass> key) {
    return super.containsKey(key);
}

要确定@SuppressWarnings 的范围，您可以将实现委托给未注释@EnsuresNonNullIf 的方法。

Answer 2

当你说

Java 规范声明 get(...) 方法在 地图不包含该键的条目

你是对的，但只是部分正确，check here，javadoc 声明，

如果此映射允许 null 值，则 null 返回值不允许 必然表明该映射不包含该键的映射； 映射也可能将键显式映射为空。这 containsKey 操作可以用来区分这两种情况。

这意味着，如果您将键映射到空值，您的方法 containsKeyStrict 可能会返回 true，但您的方法 getStrict 仍然会返回 null，而不是因为该键没有值但是因为该键的值恰好是null。

要强制执行您需要的那种行为，您可以使用不允许空值（或键）的HashTable，或者您可以向put 方法添加验证以防止插入null值到你的地图，祝你好运。