代碼契約問題

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對類不變式有很好的解釋。