代码之家 › 专栏 › 技术社区 › Dan Bryant

为什么这个代码不能证明?

code-contracts static-analysis c#

Dan Bryant · 技术社区 · 16 年前

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

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

    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() 也不为空。我错过了什么?

附加信息:返回IEnumerable的方法是通过yield return调用实现的。我在想,也许枚举器魔法在某种程度上扰乱了代码契约。。。

我只是尝试将实现更改为返回一个空数组,而不是使用yield return,这样就可以传递契约,所以显然这是使用yield return的方法的问题。有人知道怎么解决这个问题吗?

.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)。

1 回复 | 直到 16 年前

Jon Skeet 16 年前

我 犯罪嫌疑人 这是因为合同电话最后都在电话亭里 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

如果我听说代码合同团队正在解决这个问题,我不会感到惊讶。。。我想我听说过类似的事情,但我记不清细节了。这个 release notes

对迭代器上契约的初始支持

... 但假设您使用的是最新版本,那么初步支持可能还不够:)