코드 계약에서 Contract.ForAll 사용

Question

그래, 또 다른 코드 계약 질문이 있습니다.

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

I 코드 다음과 같다 인터페이스 소모가 :

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

AddRequested이 비를 요구 I는 (다른 방법이 명료 함을 위해 생략)이 보이는 인터페이스 방법에 대한 계약을 가지고 null 입력 매개 변수 (그것은 Requires 계약이있는 인터페이스를 구현합니다.) 따라서 서브 그룹에 AddRequested으로 전달되는 'required unproven : group! = null'오류가 발생합니다. ForAll 구문을 올바르게 사용하고 있습니까? 그렇다면 솔버는 단순히 이해하지 못한다. 솔버가 계약을 인식하는 데 도움이되는 또 다른 방법이 있는가? 아니면 GetAllGroups()가 호출 될 때마다 Assume을 사용하기 만하면 되는가?

Answer 1

Code Contracts User Manual은 "정적 계약 검사기는 아직 양자에 대한 ForAll 또는 Exists를 처리하지 않습니다."라고 명시합니다. 그럴 때까지는 옵션이 다음과 같습니다.

1. 경고를 무시하십시오.
2. AddRequested()으로 전화하기 전에 Contract.Assume(subGroup != null)을 추가하십시오.
3. AddRequested()으로 전화하기 전에 수표를 추가하십시오. 어쩌면 if (subGroup == null) throw new InvalidOperationException() 또는 if (subGroup != null) AddRequested(subGroup) 일 수 있습니다.

옵션 1은 실제로 도움이되지 않습니다. 옵션 2는 AddRequested()을 우회하기 때문에 위험합니다 IUnboundTagGroup.GetAllGroups()이 더 이상 사후 조건을 보장하지 않더라도 계약이 필요합니다. 나는 옵션 3을 가지고 갈 것이다.