需要什麼證明本合同。需要？

我有過幾輪比賽運行的應用程序，而我對這個簡單的代碼結構得到一個合同警告：需要什麼證明本合同。需要？

public static void LoadState(IList<Object> stuff) 
    { 
     for(int i = 0; i < stuff.Count; i++) 
     { 
      // Contract.Assert(i < stuff.Count); 
      // Contract.Assume(i < stuff.Count); 

      Object thing = stuff[i]; 

      Console.WriteLine(thing.ToString()); 
     } 
    }

的警告是：

contracts: requires unproven: index < @this.Count

我在做什麼錯誤？我如何在IList<T>上證明這一點？這是靜態分析器中的一個錯誤嗎？我將如何向微軟提交錯誤報告？

來源

2009-08-04 John Gietzen

我檢查了代碼合同1.2.21023.14版本並沒有得到警告。我的猜測是，這是一個已經修復的錯誤。

來源

2009-10-31 18:04:25 hwiechers

很高興知道。將檢查框架的第4版。 – 2009-11-01 01:53:24

這看起來很奇怪。不幸的是，我使用代碼合同的VS2010 Pro版本，所以我無法運行cccheck自己玩。

你肯定需要索引而不是僅僅使用foreach循環嗎？

可以肯定的是，您上面的簡化示例會產生相同的錯誤嗎？總是有必要檢查簡化是否解決了問題:)例如，您是否還有其他任何stuff合同檢查器可能用來使關於stuff.Count的擔保無效？

來源

2009-08-04 21:59:37

是的，我檢查了這個簡化版本的確如此。我這是靜態檢查器中的一個錯誤。在這種情況下，我*可以*使用枚舉，但對我來說，「正確的方式」似乎是通過索引訪問（因爲我以有序的方式訪問它）。 – 2009-08-05 14:03:55

當您訪問它時，會定購'foreach'一個自然有序的集合雖然（如列表）。你只需要擔心訂購失敗的事情，如套。但是，這不在重點。如果您取消註釋每條註釋行，會發生什麼情況？ – 2009-08-05 14:32:15

也沒有效果。這正是我認爲這可能是一個錯誤的原因。 – 2009-08-05 14:54:44

需要什麼證明本合同。需要？

回答

相關問題