如何提示靜態檢查器以瞭解簡單的算術操作？

我正在將一個位圖封裝爲一個像素數組的對象。該數組是一維的，我將圖像的寬度存儲在只讀字段中。我還添加了一個根據像素數組長度和寬度計算高度的屬性。我有以下關於高度的不變式：如何提示靜態檢查器以瞭解簡單的算術操作？

像素數組（Data屬性，使用私有數據字段）不爲空，並且至少有一個元素。
寬度大於零

height屬性的代碼：

public int Height 
{ 
    [Pure] 
    get 
    { 
     Contract.Requires(Data != null); 
     Contract.Requires(Width > 0); 
     Contract.Requires(Data.Length > 0); 

     Contract.Ensures(Contract.Result<int>() > 0); 
     Contract.EndContractBlock(); 
     Contract.Assume(Data.Length > Width); 

     return Data.Length/Width; 
    } 
}

但我不能讓靜態檢查證明的保證。問題可能是（根據我的理解），沒有要求Data.Length % Width == 0，因爲整數除分Data.Length/Width可能爲零;因此我增加了沒有運氣的假設。我不知道如何提示靜態檢查器接受我的確保。

來源

2012-12-22 WebMonster

我寫了一個簡單的小測試，似乎傳遞

測試對象類：

public class Class1 
{ 
    public int Width { get; set; } 
    public byte[] Data { get; set; } 

    public int Height 
    { 
     [Pure] 
     get 
     { 
      Contract.Requires(Data != null); 
      Contract.Requires(Width > 0); 
      Contract.Requires(Data.Length > 0); 

      Contract.Ensures(Contract.Result<int>() > 1); 
      //Contract.Assume(Data.Length > Width); 

      return Data.Length/Width; 
     } 
    } 
}

單元測試：

[TestFixture] 
public class Tests 
{ 
    [Test] 
    public void Class1_ContractEnsures_IsEnforced() 
    { 
     var item = new Class1 { Width = 1, Data = new byte[1] }; 
     var h = item.Height; 
    } 
}

需要注意的是，如果我再 - 啓用Assume約束，那麼這將首先觸發（並失敗），因此Ensures不會被測試。包括單元測試以創建對Height的呼叫。沒有這個，代碼合同似乎檢測到Height未被使用，所以不會應用確保約束。此外，我收到的錯誤消息是CodeContracts: requires is false這可能有點誤導。

我使用Code Contracts 1.4.50327.0如果有幫助嗎？

來源

2012-12-24 01:16:31 Mightymuke

如何提示靜態檢查器以瞭解簡單的算術操作？

回答

相關問題