代码契约问题

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

这保证了当RandomMethod被执行randomString将不能为空。为什么代码合同分析忽略了这个事实并且引发CodeContracts: requires unproven: replacement != null警告？

Answer 1

分析仪可能不会忽略这样一个事实，即它无法建立两种方法之间的联系。

属性“字段randomString非空”是一个类不变：它在每个实例创建成立，并保留平凡的每个方法调用，因为该领域是只读的。我敦促你提供一个说明。它将很容易被分析仪验证，并将提供必要的假设证明RandomMethod是安全的。

This page对类不变式有很好的解释。