계약은 정적 분석을 잘못 여기 ... 나는이 문제에 대한 몇 시간을 보냈어요 조건을

Question

를 확인하지 않다고 생각하는 것은 내 코드입니다 "ensures unproven: Contract.ForAll<string>(Contract.Result<IEnumerable<string>>(), s => s != null)"으로 신고되었습니다. 어떻게 그럴 수 있는지 모르겠다 - 그것이 null 항목을 반환하지 않을 것이라는 보장을 생성하고, 분석기는 그것에 대해 불평하지 않는다. 내가 도대체 ​​뭘 잘못하고있는 겁니까?

[편집] 흠 ... 갑자기 나는 Generate 함수에 대한 경고를받습니다. 똑같은, 보장은 입증되지 않았습니다. 나는 이것이 전에는 일어나지 않았다고 맹세할 수 있었지만, 어쨌든 문제는 이제 움직였다. 분석기가 null 항목을 반환 할 방법이 없다는 것을 어떻게 설득 할 수 있습니까? 또는 양자 택일로, 내가 틀렸고 기능은 수 있습니다 null 항목을 반환합니까?

[편집] Blech ... this article은 "사후 조건 (즉, Contract.Ensure)이 정적 검사기에서 지원되지 않습니다."(반복기에서) ... 누구나 확인할 수 있습니까?

Answer 1

yield return은 현재 컴파일러와 ccrewrite 간의 상호 작용으로 인해 Contract.Ensures과 작동하지 않습니다.

당신이 지금 할 수있는 베스트 계약없이 개인 방법을 작성하는 것입니다 및 공개 방법 다음 Assume 필요한 계약 :

private static IEnumerable<T> RealGenerate<T>(this Func<T> generator) where T : class 
{ 

    if (generator == null) 
    yield break; 

    T t; 
    while ((t = generator()) != null) 
    yield return t; 
} 

public static IEnumerable<T> Generate<T>(this Func<T> generator) where T: class 
{ 
    Contract.Ensures(Contract.Result<IEnumerable<T>>() != null); 
    Contract.Ensures(Contract.ForAll(Contract.Result<IEnumerable<T>>(), item => item != null)); 

    var result = RealGenerate(generator); 
    Contract.Assume(result != null); 
    Contract.Assume(Contract.ForAll(result, item => item != null)); 
    return result; 
}