0
  • マップのような機能を持つインターフェイスがありますが、Java の Map インターフェイスを実装していません。
  • マップ インターフェイスも実装しIterable<Object>ます。マップのキーを反復します
  • this強化されたループ (以下を参照) の本体で使用したいと思いますが、アサーションは使用getせず、反復キーの値を取得するために使用し[ERROR]、Checker フレームワークから を使用しません。
  • それはまったく可能ですか?どこから始めるべきか、または学ぶべき例を教えていただけますか? 無計画に sを散りばめようと@KeyForしましたが、自分が何をしているのかを完全に理解していないため、適切な場所に到達するまでに時間がかかる可能性があります ;-)
  • 「エントリ イテレータ」を使用して、そもそもこの問題を解決する必要がないようにすることは理解していますが、キー イテレータとメソッドの間のセマンティックな関係についてチェッカー フレームワークに教える方法を学ぶことに本当に興味があります@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

互換性のない 2 つの仕様は次のとおりです。

  1. put@NonNullnull 以外の 2 番目の引数が必要です (これがデフォルトであることを思い出してください)。
   public IMap put(Object key, Object value) { ... }
  1. getいつでも null を返す可能性があり、クライアントは戻り値がいつ null 以外になるかを知る方法がありません。
   @Nullable Object get(Object o);

メソッドの戻り値が一般に null 可能であるが、特定の状況では null ではないことを示したい場合は、などの条件付き事後条件@EnsuresNonNullIfを使用する必要があります。

とはいえ、Nullness Checker にはに対する特別な処理がありMap.getます。オーバーライドするメソッドがないため、コードはそれを使用しません(ただし、 とは関係のないjava.util.Map.getという名前のクラスがあります)。Mapjava.util.Map

の特別なケースの処理が必要な場合はIMap.get、次のいずれかを行います。

  • あなたのクラスは拡張する必要がありますjava.util.Map、または
  • クラスを認識するように Nullness Checker を拡張する必要があります。

マップキーの問題

どこから始めるべきか、または学ぶための例を教えていただけますか?

Checker Framework Manualから始めることをお勧めします。たくさんの説明と例があります。少なくともMap Key Checker の章を読む必要があります。Javadoc for@KeyForなどの詳細なドキュメントにリンクしています。

行き当たりばったりに @KeyFors を散りばめようとしましたが、自分が何をしているのかを完全に理解していないため、適切な場所に到達するまでに時間がかかる可能性があります ;-)

お願い、それはやめて！その道には苦しみがあります。マニュアルにはそうしないように書かれています。代わりに、まず考えて、コードを説明する仕様を記述してください。

以下に@KeyFor、あなたが書き留める 3 つの注釈を示します。

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. イテレータは、このオブジェクトのキーを返します。このオブジェクトは含まれているオブジェクトのラッパーとして機能するため、警告を抑制しました。チェッカー フレームワークには、「このオブジェクトはフィールドのラッパーであり、そのメソッドのそれぞれが同じプロパティを持っている」と言う方法があることを思い出せません。そのフィールドのメソッドとして。」

結果の型チェックは問題なく行われます (この回答の最初のセクションに記載されている nullness を除く)。

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 に答える