12

わかりました、コード コントラクトに関する別の質問があります。私は次のようなインターフェイス メソッドのコントラクトを持っています (明確にするために他のメソッドは省略されています)。

[ContractClassFor(typeof(IUnboundTagGroup))]
public abstract class ContractForIUnboundTagGroup : IUnboundTagGroup
{
    public IUnboundTagGroup[] GetAllGroups()
    {
        Contract.Ensures(Contract.Result<IUnboundTagGroup[]>() != null);
        Contract.Ensures(Contract.ForAll(Contract.Result<IUnboundTagGroup[]>(), g => g != null));

        return null;
    }
}

次のようなインターフェイスを使用するコードがあります。

    public void AddRequested(IUnboundTagGroup group)
    {
            foreach (IUnboundTagGroup subGroup in group.GetAllGroups())
            {
                AddRequested(subGroup);
            }
            //Other stuff omitted
    }

AddRequestednull 以外の入力パラメーターが必要なため (Requires コントラクトを持つインターフェイスを実装する)、渡される subGroup で「requires unproven: group != null」エラーが発生しますAddRequested。ForAll 構文を正しく使用していますか? そうであり、ソルバーが単に理解していない場合、ソルバーがコントラクトを認識できるようにする別の方法はありますか、または GetAllGroups() が呼び出されるたびに Assume を使用する必要がありますか?

4

1 に答える 1

10

コード コントラクトのユーザー マニュアルには、「静的コントラクト チェッカーは、ForAll または Exists の数量をまだ処理していません」と記載されています。それまでは、オプションは次のように思われます。

  1. 警告を無視します。
  2. Contract.Assume(subGroup != null)への呼び出しの前に追加しAddRequested()ます。
  3. への呼び出しの前にチェックを追加しAddRequested()ます。多分if (subGroup == null) throw new InvalidOperationException()またはif (subGroup != null) AddRequested(subGroup)。

オプション 1 はあまり役に立ちません。オプション 2 は、事後条件が保証されなくなったAddRequested()としても Requires コントラクトを回避するため、危険です。IUnboundTagGroup.GetAllGroups()私はオプション3で行きます。

于 2010-06-25T08:42:29.780 に答える