Code des marchés

Question

problème

Considérez le code suivant:

public class RandomClass 
{   
    private readonly string randomString; 

    public RandomClass(string randomParameter) 
    { 
     Contract.Requires(randomParameter != null); 
     Contract.Ensures(this.randomString != null); 

     this.randomString = randomParameter; 
    } 

    public string RandomMethod() 
    { 
     return // CodeContracts: requires unproven: replacement != null 
      Regex.Replace(string.Empty, string.Empty, this.randomString); 
    } 
} 

Cela garantit que randomString ne sera pas nulle quand RandomMethod est exécuté. Pourquoi l'analyse des contrats de code ignore-t-elle ce fait et émet un avertissement CodeContracts: requires unproven: replacement != null?

Answer 1

Ce n'est probablement pas tant que l'analyseur ignore le fait qu'il est incapable de faire le lien entre les deux méthodes. La propriété "champ randomString est non nul" est un invariant de classe: il est établi à chaque création d'instance, et trivialement conservé à chaque appel de méthode car le champ est en lecture seule. Je vous exhorte à en fournir un en indiquant cela. Il sera facilement vérifié par l'analyseur et fournira l'hypothèse nécessaire pour prouver que RandomMethod est sûr.

This page a une bonne explication sur les invariants de classe.