Код контрактов проблема

Question

Рассмотрим следующий код:

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);
    }
}

Это гарантирует, что randomString не будет нулевым при выполнении RandomMethod. Почему анализ контрактов кода игнорирует этот факт и выдает CodeContracts: requires unproven: replacement != null предупреждение?

Answer 1

Вероятно, анализатор игнорирует тот факт, что он не может установить связь между двумя методами.

Свойство «field randomString is non-null» является инвариантом класса : оно устанавливается при каждом создании экземпляра и тривиально сохраняется при каждом вызове метода, поскольку поле доступно только для чтения. Я призываю вас предоставить один, утверждающий только это. Он будет легко проверен анализатором и предоставит гипотезу, необходимую для доказательства безопасности RandomMethod.

На этой странице есть хорошее объяснение инвариантов классов.