代碼合同 - 靜態檢查器不會獲得可空類型？

Question

我想我在靜態合同檢查工具中發現了一個錯誤。除了用[ContractVerification(false)]標記整個事物之外，還有其他方法嗎？

class Employee 
{ 
    public int? HierarchyLevel { get; private set; } 

    public Employee(int? level) 
    { 
     Contract.Requires<ArgumentException>(
      (!level.HasValue) 
      || 
      level >= 0 && level <= 10); 
     Contract.Ensures(
      (!HierarchyLevel.HasValue) 
      || 
      (HierarchyLevel.Value >= 0 && HierarchyLevel.Value <= 10)); 
     this.HierarchyLevel = level; //unproven 

     // this doesnt work either 
     //if (!level.HasValue) { 
     // this.HierarchyLevel = new Nullable<int>(); 
     //} else { 
     // this.HierarchyLevel = new Nullable<int>(level.Value); 
     //} 

     // can't even make the static checker shut up with that: 
     //Contract.Assume(
     // (!HierarchyLevel.HasValue) 
     // || 
     // (HierarchyLevel.Value >= 0 && HierarchyLevel.Value <= 10)); 
    } 
} 

令人驚訝的是，下面的版本工作。但我不想開始編寫單向代碼或引入我自己的Nullable版本來取悅合同驗證工具。

class Employee2 
{ 
    public int HierarchyLevel { get; private set; } 
    public bool HasLevel { get; private set; } 
    public Employee2(int level, bool hasLevel) 
    { 
     Contract.Requires<ArgumentException>(!hasLevel || level >= 0 && level <=10); 
     if (hasLevel) { 
      HasLevel = true; 
      HierarchyLevel = level; 
     } else { 
      HasLevel = false; 
      HierarchyLevel = -1; 
     } 
    } 
    [ContractInvariantMethod] 
    private void ObjectInvariant() 
    { 
     Contract.Invariant(
      (!HasLevel) || 
      (HierarchyLevel >= 0 && HierarchyLevel <= 10)); 
    } 
} 

Answer 1

首先，你已經在你的代碼放錯地方的一些大括號（但這並不解決您的問題）：

Contract.Requires<ArgumentException>(!level.HasValue 
    || (level.Value >= 0 && level.Value <= 10)); 
Contract.Ensures(!HierarchyLevel.HasValue 
    || (HierarchyLevel.Value >= 0 && HierarchyLevel.Value <= 10)); 

我想你可能是正確的：靜態檢查不能證明一切尚未，也取決於基礎類庫。 this thread中的人似乎在談論靜態檢查器如何由於可空類型的合同實現中的錯誤而無法正確理解可空類型。

當然，你也可以寫出如下，解決你的問題：

Contract.Requires<ArgumentException>(!level.HasValue 
    || (level.Value >= 0 && level.Value <= 10); 
Contract.Ensures(HierarchyLevel == level); 

這裏是另一個解決您的問題。將條件放入單獨的方法中，並用PureAttribute（表明該方法沒有副作用）標記該方法。然後，對傳入參數和保證值應用該方法，如下所示：

[Pure] 
public static bool IsInRange(int? value) 
{ 
    return !value.HasValue 
     || (value >= 0 && value <= 10); 
} 

public Employee(int? level) 
{ 
    Contract.Requires<ArgumentException>(IsInRange(level)); 
    Contract.Ensures(IsInRange(HierarchyLevel)); 
    this.HierarchyLevel = level; 
}