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()。我的方法声明它确保结果不为空，所以这似乎意味着源ToArray()也不为空。我错过了什么？

附加信息：返回 IEnumerable 的方法是通过 yield return 调用实现的。我想知道枚举器的魔法是否会以某种方式弄乱代码合同......

我只是尝试更改实现以返回一个空数组而不是使用 yield return 并通过合同，所以显然这是使用 yield return 的方法的问题。有人知道解决这个问题的方法吗？

我查看了 Contracts 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 返回一个布尔值）。

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;
}

这有点低效，因为它将执行两次无效检查。它也有效地只是通过抑制警告Assume。

听到代码合同团队正在努力解决这个问题，我不会感到惊讶……我想我听说过类似的事情，但我不记得细节了。2009 年 9 月版本的发行说明包括：

对迭代器合约的初始支持

...但假设您使用的是最新版本，大概最初的支持是不够的 :)

于 2010-06-23T16:22:23.697 回答