Contrats de code: Pourquoi certains invariants ne sont-ils pas considérés en dehors de la classe?

Question

Tenir compte de ce type immuable:

public class Settings 
{ 
    public string Path { get; private set; } 

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

    public Settings(string path) 
    { 
     Contract.Requires(path != null); 
     Path = path; 
    } 
} 

Deux choses à remarquer ici:

• Il y a un contrat invariant qui garantit la propriété Path ne peut jamais être null
• Le constructeur vérifie la valeur de l'argument path respecter l'invariant du contrat précédent

À ce stade, une instance Setting ne peut jamais avoir une propriété nullPath.

Maintenant, regardez ce type:

public class Program 
{ 
    private readonly string _path; 

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

    public Program(Settings settings) 
    { 
     Contract.Requires(settings != null); 
     _path = settings.Path; 
    } // <------ "CodeContracts: invariant unproven: _path != null" 
} 

Fondamentalement, il a son propre contrat invariant (sur le champ _path) qui ne peut être satisfaite lors de la vérification statique (commentaire voir ci-dessus). Cela semble un peu bizarre pour moi, car il est facile de le prouver:

• settings est immuable
• settings.Path ne peut pas être nulle (parce que les paramètres a le contrat correspondant invariant)
• en assignant settings.Path à _path, _path ne peut pas être nul

J'ai manqué quelque chose ici?

Answer 1

Après avoir vérifié la code contracts forum, j'ai trouvé this similar question avec la réponse suivante à partir de l'un des développeurs:

Je pense que le comportement que vous rencontrez est causée par une inférence entre méthode qui se passe. Le vérificateur statique analyse d'abord les constructeurs, puis les propriétés puis les méthodes. Lors de l'analyse du constructeur de Sample, il ne sait pas que msgContainer.Something! = Null alors il émet l'avertissement. Une façon de le résoudre, soit en ajoutant une hypothèse msgContainer.Something! = Null dans le constuctor, ou mieux d'ajouter le postcondition! = Null à quelque chose.

En d'autres termes, vos options sont:

1. Faire la place explicite la propriété de Settings.Path automatique et spécifiez l'invariant sur le champ de support à la place. Afin de satisfaire votre invariant, vous devrez ajouter une précondition à l'accesseur set de la propriété: Contract.Requires(value != null).

   Vous pouvez éventuellement ajouter un postcondition à l'accesseur get avec Contract.Ensures(Contract.Result<string>() != null), mais le vérificateur statique ne se plaint pas de toute façon.

2. Ajouter Contract.Assume(settings.Path != null) au constructeur de la classe Program.

Answer 2

Les invariants ne fonctionnent pas sur les membres privés, vous ne pouvez pas en avoir la raison, espérons que cela vous aide.