Comment indiquer au vérificateur statique qu'une propriété ne change jamais lorsqu'elle n'est pas prouvée?

Question

Ma classe a une propriété qui est initialisée dans le constructeur et qui n'est jamais censée changer. Les méthodes tout autour de mon code acceptent cette classe comme un paramètre et s'appuient sur cette propriété pour satisfaire une certaine condition.

Le point clé est qu'il est vraiment indémontrable que la propriété ne change jamais. Je peux personnellement "jurer" qu'il ne change jamais (et j'ai aussi des tests unitaires pour cela), mais cela ne peut pas être prouvé formellement (ou du moins je le pense).

Prenons l'exemple suivant réduit:

public class ConstantPoperty 
    { 
     public class SomeClass 
     { 
      public int SomeProp { 
       get { return GetSomePropThroughUnprovableMechanism(); } 
      } 

      public SomeClass(int i) 
      { 
       SetSomePropThroughUnprovableMechanism(i); 
      } 
     } 

     public void Method(SomeClass c) 
     { 
      Contract.Requires(c != null); 
      Contract.Requires(c.SomeProp == 5); 
     } 

     public void FalsePositive() 
     { 
      SomeClass c = new SomeClass(5); 
      if (c.SomeProp != 5) return; 
      Method(c); 
      Method(c); // unproven requires: c.SomeProp == 5 
     } 
    } 

Notez que le premier appel à Method() obtenir un OK du vérificateur, puisque je l'ai vérifié juste avant que la condition qu'il soit satisfait.
Toutefois, le deuxième appel reçoit un avertissement non prouvé. Ma supposition est, le vérificateur suppose que le premier appel à Method(c) pourrait changer c.SomeProp de sorte qu'il ne satisfera plus la condition.

De là, je peux en déduire deux solutions de contournement possibles, ni dont je considère acceptable:

1. Ajouter Contract.Ensures(c.SomeProp == Contract.OldValue(c.SomeProp))-Method, ainsi que toute autre méthode qui accepte des arguments de type SomeClass.
   On peut facilement voir à quel point c'est absolument ridicule.

2. Ajoutez un contrôle redondant pour c.SomeProp == 5 avant le deuxième appel à Method(c).
   Bien que ce soit moins ridicule que la première option, elle est également inacceptable, car en plus d'encombrer le code, elle aura également une pénalité de performance (une telle vérification ne sera pas optimisée).

La solution idéale serait de convaincre en quelque sorte le vérificateur que SomeProp est censé ne jamais changer après la construction, mais je ne pouvais pas trouver un moyen de le faire. Ou peut-être qu'il me manque quelque chose d'évident ici?

Answer 1

Réécrire comme ceci:

public class SomeClass 
{ 
    private readonly int _someProp; 

    public int SomeProp { get { return _someProp; } } 

    public SomeClass(int i) 
    { 
     _someProp = i; 
    } 
}