C＃代碼合同：爲什麼不能證明這個簡單的條件？

Question

我正在做一個簡單的代碼合同測試。下面的代碼是在一個winform中。這傳遞（當然）：

private void Test(Form form) 
    { 
     Contract.Requires(!string.IsNullOrEmpty(form.Name)); 

     MessageBox.Show(form.Name); 
    } 

    protected override void OnLoad(EventArgs e) 
    { 
     if (!string.IsNullOrEmpty(Name)) 
      Test(this); 

     base.OnLoad(e); 
    } 

不過，我增加一個間接的只是一個很簡單的層面，它說：「需要得到證實」：

private bool Valid(string str) 
    { 
     return !string.IsNullOrEmpty(str); 
    } 

    protected override void OnLoad(EventArgs e) 
    { 
     if (Valid(Name)) 
      Test(this); 

     base.OnLoad(e); 
    } 

這似乎將是微不足道的證明。爲什麼它不工作？

Answer 1

您的Valid方法沒有得到任何合同。你可以在那裏表達一份合同，這可能與代碼是一樣的，真​​的......但是代碼合同不會假設這一點。您的實施可能會發生變化 - 您還沒有告訴代碼合同，意味着要做什麼，所以它不會假定實施中的任何內容。

Answer 2

你真的需要一個方法來調用string.IsNullOrEmpty(str)嗎？而且由於String.IsNullOrEmpty(string)已在BCL中標記爲[Pure]，並且由於包裝是無關的，所以如果直接調用它，整個問題就會消失。

如果你真的非常希望這種方法，那麼這可能與當前的代碼打交道的一個辦法是改變你的Test方法您的合同：

private void Test(Form form) 
{ 
    Contract.Requires(Valid(form.Name)); 

    MessageBox.Show(form.Name); 
} 

[Pure] 
private bool Valid(string str) 
{ 
    return !string.IsNullOrEmpty(str); 
} 

現在的靜態分析不應該抱怨。