none
Contracts.Ensureについて RRS feed

  • 質問

  • コードコントラクを使ってC#での開発を行っている者です。
    VS2010Proを使用しております。
    以下のようなコードを作成すると。
    Console.WriteLine(a.Length);
    の部分で、警告が出力されてしまうのですが、
    CodeContracts: Possibly calling a method on a null reference 'a
    これはどうやって抑制すればよいでしょうか。
    いちよう、
    Contract.Ensures(Contract.ForAll(Contract.Result<IEnumerable<string>>(), st => st != null));
    と宣言しているため、aはnullではない、と解釈されるハズだと理解しています。

    宜しくお願い致します。

    public static IEnumerable<string> GetStringList()
    {
    Contract.Ensures(Contract.Result<IEnumerable<string>>() != null);
    Contract.Ensures(Contract.ForAll(Contract.Result<IEnumerable<string>>(), st => st != null));

    List<string> list = new List<string>();
    list.Add("abc");
    list.Add("def");
    return list;
    }

    public static void TestFunc()
    {
    IEnumerable<string> test = GetStringList();
    foreach (string a in test)
    {
    Console.WriteLine(a.Length);
    }
    }


    2010年11月17日 4:32

すべての返信

  • Contract.Result は戻り値を確認するものであって、その検証ブロックの出力を保証するものではありませんよね? 「検証済みの安全な入力」などという都合のよい(わるい?)解釈はなく、「安全な入力であることを検証する」ことが目的ですので、TestFunc のブロックにおいて test や a が正しい入力であることは別途検証しなければならないと思います。

    2010年11月17日 7:07
  • いえ、Contract.Resultではなく、Contract.Ensureは検証ブロックの出力を保証するものですよね。

    実際

    Contract.Ensures(Contract.Result<IEnumerable<string>>() != null);

    があるため、

    foreach (string a in test)

    では警告が出力されていません。実際、前者のEnsureを外した場合、以下のようにしないと警告が解除できません。

    これは、出力を保証しているということだと思っていたのですが……

    public static void TestFunc()
    {
    IEnumerable<string> test = GetStringList();
        if (test != null)
    {
    foreach (string a in test)
    {
    Console.WriteLine(a.Length);
    }
    }
    }
    2010年11月17日 9:38
  • Code Contracts はほとんど把握できていないので、見当違いでしたらすみません。
    IEnumerable.GetEnumerator で取得できる IEnumerator や、それの IEnumerator.Current は、前回の列挙時と同じとは限らない(実装次第)と思うのですが、それは関係ないでしょうか?
    2010年11月18日 2:16
  • Result を Ensure した結果ってちゃんと流れるんですね。

    おそらく、問題は、Ensures に与えてる式の「仮引数 st」が「Result の従要素」であると CodeContracts に認識されていないからではないでしょうか。(また、どのような子要素であるかも)

    戻り値を配列にして、インデックスを用いて配列の中身を検査した場合には問題ないようでしたので、Ensures に与える式をどのようにして Result に関連付けるか、Result オブジェクトの何を事後検証したのかがポイントなのではないかと思います。

    2010年11月24日 3:41