1

次のように開始するメソッドがあります。

    public static UnboundTag ResolveTag(Type bindingType, string name, string address)
    {
        Contract.Requires(bindingType != null);

        var tags = GetUnboundTagsRecursively(bindingType).ToArray();

GetUnboundTagsRecursively の実装のコントラクト (同じクラスで実装) は次のようになります。

    public static IEnumerable<UnboundTag> GetUnboundTagsRecursively(Type bindingType)
    {
        Contract.Requires(bindingType != null);
        Contract.Ensures(Contract.Result<IEnumerable<UnboundTag>>() != null);

静的アナライザーは、ResolveTag のタグ割り当て行での失敗をメッセージで示しています"requires unproven: source != null"。私はこれを数回調べましたが、なぜこれが起こるのかわかりません。sourceこれは、拡張メソッドのパラメーターへの参照であると想定していますToArray()。私のメソッドは、結果が null ではないことを保証すると述べているため、これは、のソースToArray()も null ではないことを暗示しているように思われます。私は何が欠けていますか？

追加情報: IEnumerable を返すメソッドは、yield リターン コールで実装されています。列挙子の魔法が何らかの形でコード契約をいじっているのではないかと思っています...

yield return を使用するのではなく、空の配列を返すように実装を変更しようとしましたが、それはコントラクトを渡します。明らかに、yield return を使用するメソッドの問題です。誰もこれを回避する方法を知っていますか?

コントラクト DLL の IL を調べたところ、実際には、列挙子の実装のためにコントラクト呼び出しが MoveNext() に配置されています。

.method private hidebysig newslot virtual final 
        instance bool  MoveNext() cil managed
{
  .override [mscorlib]System.Collections.IEnumerator::MoveNext
  // Code size       410 (0x19a)
  .maxstack  3
  .locals init ([0] bool V_0,
           [1] int32 V_1)
  .try
  {
    IL_0000:  ldarg.0
    IL_0001:  ldfld      int32 PLCLink.Bind.UnboundTag/'<GetUnboundTagsRecursively>d__c'::'<>1__state'
    IL_0006:  stloc.1
    IL_0007:  ldloc.1
    IL_0008:  ldc.i4.0
    IL_0009:  beq.s      IL_0024
    IL_000b:  ldloc.1
    IL_000c:  ldc.i4.3
    IL_000d:  sub
    IL_000e:  switch     ( 
                          IL_00cd,
                          IL_018d,
                          IL_0162)
    IL_001f:  br         IL_018d
    IL_0024:  ldarg.0
    IL_0025:  ldc.i4.m1
    IL_0026:  stfld      int32 PLCLink.Bind.UnboundTag/'<GetUnboundTagsRecursively>d__c'::'<>1__state'
    IL_002b:  ldarg.0
    IL_002c:  ldfld      class PLCLink.Bind.IUnboundTagGroup PLCLink.Bind.UnboundTag/'<GetUnboundTagsRecursively>d__c'::group
    IL_0031:  ldnull
    IL_0032:  ceq
    IL_0034:  ldc.i4.0
    IL_0035:  ceq
    IL_0037:  call       void [mscorlib]System.Diagnostics.Contracts.Contract::Requires(bool)
    IL_003c:  call       !!0 [mscorlib]System.Diagnostics.Contracts.Contract::Result<class [mscorlib]System.Collections.Generic.IEnumerable`1<valuetype PLCLink.Bind.UnboundTag>>()

Contract.Result 呼び出しが実際には間違った型を使用しているため、これは興味深いことです (MoveNext が bool を返すため)。

4

1 に答える 1

2

コントラクトMoveNext()の呼び出しが、生成されたイテレータの実装型で終わっているためだと思います。これを試して：

public static IEnumerable<UnboundTag> GetUnboundTagsRecursively
   (Type bindingType)
{
    Contract.Requires(bindingType != null);
    Contract.Ensures(Contract.Result<IEnumerable<UnboundTag>>() != null);
    return GetUnboundTagsRecursivelyImpl(bindingType);
}

private static IEnumerable<UnboundTag> GetUnboundTagsRecursivelyImpl
    (Type bindingType)
{
    // Iterator block code here
}

これらのメソッドをコントラクト違反なしでコンパイルするには、少し追加の作業が必要になる場合があります。例えば：

public static IEnumerable<UnboundTag> GetUnboundTagsRecursively
   (Type bindingType)
{
    Contract.Requires(bindingType != null);
    Contract.Ensures(Contract.Result<IEnumerable<UnboundTag>>() != null);
    IEnumerable<UnboundTag> ret = GetUnboundTagsRecursivelyImpl(bindingType);
    // We know it won't be null, but iterator blocks are a pain.
    Contract.Assume(ret != null);
    return ret;
}

これは、無効チェックを 2 回実行するため、少し非効率的です。また、 を介して警告を効果的に抑制していAssumeます。

コード コントラクト チームがこの問題の修正に取り組んでいると聞いても驚かないでしょう...似たようなことを聞​​いたことがあると思いますが、詳細は思い出せません。2009 年 9 月リリースのリリース ノートには、次のものが含まれます。

イテレータのコントラクトの初期サポート

...しかし、最近のリリースを使用していると仮定すると、おそらく初期サポートでは不十分です:)

于 2010-06-23T16:22:23.697 に答える