CodeContracts : null 참조에서 메서드를 호출했을 가능성이 있음

Question

CodeContracts static analysis tool이라는 인수가 있습니다.

내 코드 :

Screenshot http://i40.tinypic.com/r91zq9.png

(ASCII version)는

이 도구는 instance.bar가 null 참조가 될 수 있음을 알려줍니다. 나는 그 반대를 믿는다.

누가 맞습니까? 어떻게 잘못했는지 증명할 수 있습니까?

Answer 1

업데이트 : 문제가있는 것 같습니다. invariants are not supported for static fields.

두 번째 업데이트 : 아래에 요약 된 방법은 currently the recommended solution입니다.

가능한 해결 방법은 보유하려는 불변량이 instance 인 Ensure의 속성을 만드는 것입니다. (물론 Ensure을 증명하려면 Assume가 필요합니다.) 일단이 작업을 완료하면 속성을 사용하면 모든 불변량을 올바르게 증명할 수 있습니다. 여기

당신의 예는이 방법을 사용하고 : 주제 끄기

class Foo 
{ 
    private static readonly Foo instance = new Foo(); 
    private readonly string bar; 

    public static Foo Instance 
    // workaround for not being able to put invariants on static fields 
    { 
     get 
     { 
      Contract.Ensures(Contract.Result<Foo>() != null); 
      Contract.Ensures(Contract.Result<Foo>().bar != null); 

      Contract.Assume(instance.bar != null); 
      return instance; 
     } 
    } 

    public Foo() 
    { 
     Contract.Ensures(bar != null); 
     bar = "Hello world!"; 
    } 

    public static int BarLength() 
    { 
     Contract.Assert(Instance != null); 
     Contract.Assert(Instance.bar != null); 
     // both of these are proven ok 

     return Instance.bar.Length; 
    } 
} 

Answer 2

CodeContracts가 맞습니다. BarLength() 메서드를 호출하기 전에 instance.bar = null을 설정하는 데 아무 것도 멈추지 않습니다.

Answer 3

나는 동의합니다. instance 및 bar은 모두 비공개이므로 CodeContracts는 instance.bar이 null로 설정되지 않음을 알 수 있어야합니다.

Answer 4

'bar'필드를 읽기 전용으로 표시하면 정적 분석기가 ctor을 실행 한 후에 그 필드가 다른 것으로 설정되지 않을 것입니다.

private static Foo instance = new Foo(); 

당신이 때문에 초기화 된 bar을 보장, 이것이 예를 생성자는 항상 정적 메서드에 액세스하기 전에 실행 한 것을 의미 것으로 가정합니다 :

Answer 5

코드는 개인 정적 초기화 된 인스턴스를 포함?

단일 스레드 케이스에서 나는 당신이 옳다고 생각합니다.

이벤트의 순서는 다음과 같습니다

1. 전화 Foo.BarLength()에
2. (이미 완료하지 않은 경우) 클래스 Foo의 정적 초기화 Foo
의 인스턴스 개인 정적 멤버 instance의
3. 정적 초기화
4. 엔트리 to Foo.BarLength()

그러나 클래스의 정적 초기화는 앱 도메인 당 한 번만 트리거됩니다. IIRC에서는 다른 정적 메소드가 호출되기 전에 이 완료되도록을 보장하기 위해 차단 기능이 없습니다.

1. 스레드 알파 : Foo.BarLength()
2. 스레드 알파에 전화 :

   그래서, 당신은이 시나리오 가질 수있다 (이미 완료하지 않은 경우) 클래스 Foo의 정적 초기화 시작을

3. 컨텍스트 스위치
4. 베타 : 전화 Foo.BarLength()
5. 베타 : 없음 클래스 Foo의 정적 초기화에 전화이 이미 진행되고 있기 때문에
6. 스레드 베타 : 입력 스레드 베타
7. Foo.BarLength()에 : null에 액세스 계약 분석기는 것을 알 수있는 방법은 없습니다 instance

정적 멤버 코드를 다중 스레드 방식으로 실행하지 않으므로 신중해야합니다.