코드 계약 정적 분석기에서 이러한 속성 getter 호출을 동일한 것으로 취급하는 이유는 무엇입니까?

Question

나는 순서를 시행하기 위해 코드 계약을 사용하여 불변의 정렬 된 단일 링크 목록 클래스를 설정하려고합니다. 나는 이것에 졸이다 몇 가지 문제로 실행 해요 :

이

[Pure, ContractVerification(true)] 
public class Hierarchy 
{ 
    private readonly object _data; 
    private readonly Hierarchy _childField; 

    public Hierarchy() { } 

    public Hierarchy(object data, Hierarchy childParameter) { 
     Contract.Requires<ArgumentNullException>(childParameter != null); 

     _data = data; 
     _childField = childParameter; 

     Contract.Assert(HasChild); 

     Contract.Assert(_childField == childParameter); 
     Contract.Assert(_childField.Data == childParameter.Data); 

     Contract.Assert(ChildProperty == _childField); 
     Contract.Assert(ChildProperty.Data == _childField.Data); //Warning -- CodeContracts: assert unproven 
    } 

    public bool HasChild { get { return _childField != null; } } 

    public object Data { 
     get { 
      Contract.Ensures(Contract.Result<object>() == _data); 
      return _data; 
     } 
    } 

    public Hierarchy ChildProperty { 
     get { 
      Contract.Requires<InvalidOperationException>(HasChild); 
      Contract.Ensures(Contract.Result<Hierarchy>() == _childField); 

      //un-commenting this line causes the assertion to succeed. 
      //Contract.Ensures(Contract.Result<Hierarchy>().Data == _childField.Data); 

      return _childField; 
     } 
    } 

    [ContractInvariantMethod] 
    private void Invariant() { 
     Contract.Invariant(HasChild == (ChildProperty != null)); 
    } 
} 

그것은 그 코드 계약이 주장 ChildProperty.Data == _childField.Data을 입증 할 수 있어야한다고 나에게 보인다. 이전의 어설 션 ChildProperty == _childField이 성공하고 동일한 객체에서 순수 Data 속성 getter를 두 번 호출하면 동일한 결과가 반환됩니다.

_childField == childParameter 및 _childField.Data == childParameter.Data이라는 (성공한) 이전 주장에 유의하십시오.

위의 두 번째 주석에서 언급했듯이 ChildProperty 게터에 후행 Contract.Ensures(Contract.Result<Hierarchy>().Data == _child.Data);을 추가하면이 문제가 해결됩니다. 이것이 우리가해야 할 모든 것임을 유의하십시오.이 경우 코드 계약은 x == y 일 때 x 및 y에 Data 게터를 호출하면 동일한 결과를 산출합니다.

이 해결 방법은이 작은 예제에서는 문제가되지 않지만 큰 클래스에서는 각 유형의 속성에 대한 사후 조건을 추가해야하는 번거 로움이 있습니다.

버그입니까? Child.Data == _child.Data을 입증 할 수있는 일부 계약 주석 또는 그 밖의 것이 누락 되었습니까? 즉, 문제를 해결할 다른 방법이 있습니까?

Answer 1

당신은 옳습니다. 이는 증명할 수 있어야하지만 정적 검사기의 제한으로 인한 것이 아닙니다.

Answer 2

Data 속성은 _data의 내용을 변경하지 않기 때문에 수 있습니까? (readonly이지만 그 내용은 여전히 ​​변경 될 수 있습니다)?

예를 들어

, 당신은이 있다고 가정 :

public object Data { 
    get { 
     Contract.Ensures(Contract.Result<object>() == _data); 
     ((SomeClass)_data).SomeProperty += 1; 
     return _data; 
    } 
} 

그런 다음 Data 두 후속 호출은 다른 결과를 얻을 것입니다.

Data 님의 get에 이것을 추가하나요?

Contract.Ensures(_data == Contract.OldValue<object>(_data));