CodeContracts: appel possible d'une méthode sur une référence nulle

Question

J'ai un argument avec le CodeContracts static analysis tool.

Mon code:

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

(ASCII version)

L'outil me dit que instance.bar peut être une référence nulle. Je crois le contraire.

Qui a raison? Comment puis-je le prouver?

Answer 1

Mise à jour: Il semble que le problème est que invariants are not supported for static fields.

2ème mise à jour: La méthode décrite ci-dessous est currently the recommended solution.

Une solution possible est de créer une propriété pour instance que Ensure s les invariants que vous souhaitez conserver. (Bien sûr, vous avez besoin de Assume pour que le Ensure soit prouvé.) Une fois que vous avez fait cela, vous pouvez simplement utiliser la propriété et tous les invariants doivent être prouvés correctement.

Voici votre exemple en utilisant cette méthode:

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 a raison. Rien ne vous empêche de définir instance.bar = null avant d'appeler la méthode BarLength().

Answer 3

Je suis d'accord avec vous. instance et bar sont tous les deux privés, donc CodeContracts devrait être capable de savoir que instance.bar n'est jamais défini sur null.

Answer 4

Si vous marquez le champ 'bar' comme étant en lecture seule, cela devrait satisfaire l'analyseur statique que le champ ne sera jamais défini après le ctor.

Answer 5

Votre code comprend une instance initialisée statique privé:

private static Foo instance = new Foo(); 

Vous présumez que cela signifie que la instance de constructeur aura toujours courir avant l'accès à toute méthode statique, assurant ainsi bar a été initialisé?

Dans le cas d'un seul filetage, je pense que vous avez raison.

La séquence des événements serait:

1. Appel à Foo.BarLength()
2. initialisation statique de classe Foo (si pas déjà terminé)
3. d'initialisation statique de membre statique privé instance avec instance de Foo
4. Entrée à Foo.BarLength()

Toutefois, l'initialisation statique d'une classe est uniquement déclenchée une fois par App Domain - et IIRC il n'y a aucun blocage pour s'assurer que est complété avant d'appeler d'autres méthodes statiques.

Donc, vous pourriez avoir ce scénario:

1. Discussion Alpha: Appel à Foo.BarLength()
2. Discussion Alpha: L'initialisation statique de classe Foo (sinon déjà terminé) commence
3. Context Switch
4. Thread Beta: Appelez à Foo.BarLength()
5. Thread Beta: Aucun appel à l'initialisation statique de classe Foo parce que c'est déjà en cours
6. Discussion Beta: Entrée Foo.BarLength()
7. Discussion Beta: L'accès à null membre statique instance

Il n'y a aucun moyen de l'analyseur de contrats peut savoir que vous ne lanceriez jamais le code d'une manière multithread, donc il doit pécher par excès de prudence.