代碼契約 - ForAll - 什麼是靜態驗證支持

Question

有很多信息，靜態檢查Contract.ForAll只有有限的或沒有支持。

我做實驗的很多，發現它可以與工作：

• Contract.ForAll(items, i => i != null)
• Contract.ForAll(items, p)其中p類型爲Predicate<T>

它不能與工作：

• 字段訪問
• 房產訪問
• 方法組（我想委託反正這裏分配）
• 實例方法調用

我問題是：

• 是什麼ForAll可以使用的其他類型的代碼？
• 代碼合同是否承諾在Contract.ForAll(items, i => i != null)被證明後，在代碼中從列表中獲取一個項目（即通過索引）時，該項目不爲空？

下面是完整的測試代碼：

public sealed class Test 
{ 
    public bool Field; 
    public static Predicate<Test> Predicate; 

    [Pure] 
    public bool Property 
    { 
     get { return Field; } 
    }  

    [Pure] 
    public static bool Method(Test t) 
    { 
     return t.Field; 
    } 

    [Pure] 
    public bool InstanceMethod() 
    { 
     return Field; 
    } 

    public static void Test1() 
    { 
     var items = new List<Test>(); 
     Contract.Assume(Contract.ForAll(items, i => i != null)); 
     Contract.Assert(Contract.ForAll(items, i => i != null)); // OK 
    } 

    public static void Test2() 
    { 
     var items = new List<Test>(); 
     Contract.Assume(Contract.ForAll(items, Predicate)); 
     Contract.Assert(Contract.ForAll(items, Predicate)); // OK 
    } 

    public static void Test3() 
    { 
     var items = new List<Test>(); 
     Contract.Assume(Contract.ForAll(items, i => i.Field)); 
     Contract.Assert(Contract.ForAll(items, i => i.Field)); // assert unproven 
    } 

    public static void Test4() 
    { 
     var items = new List<Test>(); 
     Contract.Assume(Contract.ForAll(items, i => i.Property)); 
     Contract.Assert(Contract.ForAll(items, i => i.Property)); // assert unproven 
    } 

    public static void Test5() 
    { 
     var items = new List<Test>(); 
     Contract.Assume(Contract.ForAll(items, Method)); 
     Contract.Assert(Contract.ForAll(items, Method)); // assert unproven 
    } 

    public static void Test6() 
    { 
     var items = new List<Test>(); 
     Contract.Assume(Contract.ForAll(items, i => i.InstanceMethod())); 
     Contract.Assert(Contract.ForAll(items, i => i.InstanceMethod()));// assert unproven 
    } 
} 

Answer 1

通過反編譯mscorelib.dll System.Diagnostics.Contracts我們可以看到easely Contract.ForAll是如何構建的：它需要收集和謂語。

public static bool ForAll<T>(IEnumerable<T> collection, Predicate<T> predicate) 
{ 
    if (collection == null) 
    { 
     throw new ArgumentNullException("collection"); 
    } 
    if (predicate == null) 
    { 
     throw new ArgumentNullException("predicate"); 
    } 
    foreach (T current in collection) 
    { 
     if (!predicate(current)) 
     { 
      return false; 
     } 
    } 
    return true; 
} 

所以，當你在這種情況下說Contract.ForAll(items, i => i.Field)i => i.Field是謂語

然後按照在所有的測試方法的例子，我們可以看到您提供的空單Contract.ForAll方法，該方法將返回true，因爲它將永遠不會進入該foreach塊。

採取進一步行動，如果您添加至您的列表 var items = new List<Test>() {new Test()};並再次運行該測試也將返回false您public bool Field;默認爲false

Contract.ForAll的目標是

確定集合中的所有元素是否 函數中存在

所以我的結論是，它不是關於C ontarct。對於所有不能使用的東西，它至少是您的收藏中的一個元素返回false或爲空

Answer 2

我無法找到更多工作表達式，實際上我發現即使Contract.ForAll(items, i => i != null)工作不正常（但它理解該項目在以後在同一個函數中的foreach內部使用時不爲null）。最後，我放棄了與靜態檢查器一起使用更復雜的ForAll合同的可能性。

相反，我設計了一種方法來控制哪些合同是用於靜態檢查器，哪些用於運行時檢查器。我在這裏介紹這種方法，希望對於原始問題中有趣的人有用。好處是可以編寫更復雜的合同，只能在運行時檢查這些合同，並且僅爲靜態檢查器留下可輕鬆驗證的合同（並輕鬆地保持低數量的警告）。

爲此，2建立調試需要（如果你還沒有他們），調試和調試+靜態合同，該調試打造了條件編譯符號MYPROJECT_CONTRACTS_RUNTIME定義。通過這種方式，它收到全部Contract.和RtContract.合約。其他版本只收到Contract.合同。

public static class RtContract 
{ 
    [Pure] [ContractAbbreviator] [Conditional("MYPROJECT_CONTRACTS_RUNTIME")] 
    public static void Requires(bool condition) 
    { 
     Contract.Requires(condition); 
    } 

    [Pure] [ContractAbbreviator] [Conditional("MYPROJECT_CONTRACTS_RUNTIME")] 
    public static void Ensures(bool condition) 
    { 
     Contract.Ensures(condition); 
    } 

    [Pure] [Conditional("MYPROJECT_CONTRACTS_RUNTIME")] 
    public static void Assume(bool condition) 
    { 
     Contract.Assume(condition); 
    } 
} 

public class Usage 
{ 
    void Test (int x) 
    { 
     Contract.Requires(x >= 0); // for static and runtime 
     RtContract.Requires(x.IsFibonacci()); // for runtime only 
    } 
}