CodeContracts: possibile chiamare un metodo su un riferimento null

Question

Ho una discussione con lo CodeContracts static analysis tool.

Il mio codice:

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

(ASCII version)

Lo strumento mi dice che instance.bar può essere un riferimento null. Credo il contrario.

Chi ha ragione? Come posso dimostrare che è sbagliato?

Answer 1

Aggiornamento: Sembra che il problema sia invariants are not supported for static fields.

Secondo aggiornamento: Il metodo descritto di seguito è currently the recommended solution.

Una possibile soluzione è creare una proprietà per instance che Ensure s gli invarianti che si desidera conservare. (Naturalmente, è necessario effettuare il Assume per il Ensure da provare.) Una volta fatto ciò, si può semplicemente usare la proprietà e tutti gli invarianti dovrebbero essere provati correttamente.

Ecco il vostro esempio di utilizzo di questo metodo:

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 ha ragione. Non c'è nulla che ti impedisca di impostare instance.bar = null prima di chiamare il metodo BarLength().

Answer 3

Sono d'accordo con te. instance e bar sono entrambi privati, quindi CodeContracts dovrebbe essere in grado di sapere che instance.bar non è mai impostato su null.

Answer 4

Se si contrassegna il campo 'bar' come readonly, questo dovrebbe soddisfare l'analizzatore statico che il campo non sarà mai impostato su qualcos'altro dopo l'esecuzione del ctor.

Answer 5

Il codice include un'istanza privata statica inizializzata:

private static Foo instance = new Foo(); 

Stai assumendo che questo significa l'istanza costruttore avrà sempre eseguito prima che l'accesso a qualsiasi metodo statico, quindi, garantendo bar è stato inizializzato?

Nel caso a thread singolo, penso che tu abbia ragione.

La sequenza degli eventi sarebbe:

1. Chiama per Foo.BarLength()
2. inizializzazione statico della classe Foo (se non è già completato)
3. inizializzazione statico di membro statico privato instance con istanza di Foo
4. Immissione a Foo.BarLength()

Tuttavia, l'inizializzazione statica di una classe viene attivata solo una volta per dominio App e IIRC non prevede alcun blocco per garantire che sia completato prima di chiamare qualsiasi altro metodo statico.

Quindi, si potrebbe avere questo scenario:

1. Alpha Discussione: Call to Foo.BarLength()
2. Discussione Alpha: l'inizializzazione statico della classe Foo (se non è già completato) inizia
3. Context switch
4. Thread Beta: Chiama a Foo.BarLength()
5. Beta: No Call di inizializzazione statico della classe Foo perché è già in corso
6. Discussione Beta: Entrata al Foo.BarLength()
7. Beta Discussione: L'accesso a null membro statico instance

Non c'è modo l'analizzatore contratti possono sapere che non avresti mai eseguito il codice in un modo multithread, quindi deve errare sul lato della cautela.