代碼合同應該靜態檢查器能夠檢查算術限制嗎？

（也posted on the MSDN forum - 但是，這並沒有得到多少流量，據我可以看到。）代碼合同應該靜態檢查器能夠檢查算術限制嗎？

我一直在試圖提供的Assert和Assume一個例子。下面是我得到的代碼：

public static int RollDice(Random rng) 
{ 
    Contract.Ensures(Contract.Result<int>() >= 2 && 
        Contract.Result<int>() <= 12); 

    if (rng == null) 
    { 
     rng = new Random(); 
    } 
    Contract.Assert(rng != null); 

    int firstRoll = rng.Next(1, 7); 
    Contract.Assume(firstRoll >= 1 && firstRoll <= 6); 

    int secondRoll = rng.Next(1, 7); 
    Contract.Assume(secondRoll >= 1 && secondRoll <= 6); 

    return firstRoll + secondRoll; 
}

（關於能夠在一個空引用，而不是現有的Random引用傳遞的業務純粹是教學的，當然。）

我所希望的，如果檢查員知道firstRoll和secondRoll各自在[1, 6]的範圍內，所以能夠確定總和在[2, 12]的範圍內。

這是不合理的希望嗎？我意識到這是一個棘手的業務，正在計劃可能發生的事情......但我希望檢查器足夠聰明:)

如果現在不支持，現在有沒有人知道它是否可能受支持在接近未來的未來？

編輯：我現在發現，靜態檢查器中有非常複雜的算術選項。使用「高級」文本框，我可以從Visual Studio中嘗試它們，但根據我的情況，沒有像他們所做的那樣正確的解釋。

來源

2009-08-07 Jon Skeet

喬恩，你有沒有試過直接聯繫DevLabs的傢伙？您將在本頁底部找到列出的團隊成員：http://research.microsoft.com/en-us/projects/contracts/ – 2009-08-07 11:53:35

並且他們的電子郵件地址是codconfb _at_ microsoft _dot_ com（如上所述相同的頁面）。我很想知道你的問題的答案。 – 2009-08-07 11:54:54

我認爲先在論壇上提出問題會更有禮貌......如果我沒有在論壇上或在這裏聽到回覆，我也會通過電子郵件詢問。 – 2009-08-07 12:04:18

我在MSDN論壇上有個答案。事實證明，我差不多在那裏。基本上，如果您拆分「合約」合同，靜態檢查器的效果會更好。所以，如果我們的代碼改成這樣：

public static int RollDice(Random rng) 
{ 
    Contract.Ensures(Contract.Result<int>() >= 2); 
    Contract.Ensures(Contract.Result<int>() <= 12); 

    if (rng == null) 
    { 
     rng = new Random(); 
    } 
    Contract.Assert(rng != null); 

    int firstRoll = rng.Next(1, 7); 
    Contract.Assume(firstRoll >= 1); 
    Contract.Assume(firstRoll <= 6); 
    int secondRoll = rng.Next(1, 7); 
    Contract.Assume(secondRoll >= 1); 
    Contract.Assume(secondRoll <= 6); 

    return firstRoll + secondRoll; 
}

沒有任何問題的作品。這也意味着這個例子更加有用，因爲它強調了檢查器確實與分離出來的合同更好地合作的點。

來源

2009-08-07 20:27:26

我不知道MS合同檢查工具，但範圍分析是一種標準的靜態分析技術;它被廣泛用於商業靜態分析工具來驗證下標表達式是合法的。

MS Research在這種靜態分析方面有着良好的記錄，所以我希望做這樣的範圍分析是合同檢查器的目標，即使目前沒有檢查。

來源

2009-08-07 14:10:46

代碼合同應該靜態檢查器能夠檢查算術限制嗎？

回答

相關問題