CodeContracts: Posiblemente llamar a un método en una referencia nula

Question

estoy teniendo una discusión con el CodeContracts static analysis tool.

Mi código:

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

(ASCII version)

La herramienta me dice que instance.bar puede haber una referencia nula. Yo creo lo opuesto.

¿Quién tiene razón? ¿Cómo puedo probar que está mal?

Answer 1

Actualización: Parece que el problema es que invariants are not supported for static fields.

2da actualización: El método descrito a continuación es currently the recommended solution.

Una posible solución es crear una propiedad para instance que Ensure s las invariantes que desea mantener. (Por supuesto, necesita Assume para que se pruebe el Ensure). Una vez que haya hecho esto, puede usar la propiedad y todas las invariantes deben probarse correctamente.

Ésta es tu ejemplo usando este método:

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 es el adecuado. No hay nada que le impida configurar instance.bar = null antes de llamar al método BarLength().

Answer 3

Estoy de acuerdo con usted. instance y bar son ambos privados, por lo que CodeContracts debería poder saber instance.bar nunca se establece en nulo.

Answer 4

Si marca el campo 'bar' como de sólo lectura, que debe satisfacer el analizador estático que el campo no se establece en ninguna otra cosa después se ejecuta la ctor.

Answer 5

El código incluye una instancia inicializado estática privada:

private static Foo instance = new Foo(); 

Tiene pensado que esto significa que la instancia constructor siempre tendrá correr antes de acceder a cualquier método estático, por lo tanto, asegurar bar se ha inicializado?

En el caso de un solo subproceso, creo que tienes razón.

La secuencia de eventos sería:

1. llamada a Foo.BarLength()
2. inicialización estática de la clase Foo (si no se ha completado)
3. inicialización estática del miembro estático privada instance con instancia de Foo
4. entrada a Foo.BarLength()

Sin embargo, la inicialización estática de una clase es sólo alguna vez desencadena una vez por aplicación de dominio - y IIRC no hay bloqueo para asegurarse de que es completaron antes se llaman otros métodos estáticos.

Por lo tanto, usted podría tener este escenario:

1. Tema Alfa: Llamada a Foo.BarLength()
2. Tema Alfa: inicialización estática de la clase Foo (si no se ha completado) comienza
3. cambio de contexto
4. Subproceso Beta: llame al Foo.BarLength()
5. Subproceso Beta: No Llamar de inicialización estática de la clase Foo porque eso es ya en marcha
6. rosca Beta: Entrada a Foo.BarLength()
7. rosca Beta: El acceso a null miembro estático instance

No hay manera de que el analizador contratos puede saber que nunca ejecutarías el código de manera multiproceso, por lo que tiene que pecar de cauteloso.