在代碼合同中使用Contract.ForAll

好的，我還有另一個代碼合同問題。我有一個接口方法的合同，看起來像這樣（爲清楚起見省略其它方法）：在代碼合同中使用Contract.ForAll

[ContractClassFor(typeof(IUnboundTagGroup))] 
public abstract class ContractForIUnboundTagGroup : IUnboundTagGroup 
{ 
    public IUnboundTagGroup[] GetAllGroups() 
    { 
     Contract.Ensures(Contract.Result<IUnboundTagGroup[]>() != null); 
     Contract.Ensures(Contract.ForAll(Contract.Result<IUnboundTagGroup[]>(), g => g != null)); 

     return null; 
    } 
}

我有代碼消耗看起來像這樣的接口：

public void AddRequested(IUnboundTagGroup group) 
    { 
      foreach (IUnboundTagGroup subGroup in group.GetAllGroups()) 
      { 
       AddRequested(subGroup); 
      } 
      //Other stuff omitted 
    }

AddRequested需要非空輸入參數（它實現了一個接口有一個需求合同），所以我得到一個'需要未經證實：組！=空'錯誤的子組被傳遞到AddRequested。我是否正確使用ForAll語法？如果是這樣，求解者根本不理解，還有另一種方法可以幫助求解器識別合同，或者每當調用GetAllGroups（）時，我是否只需要使用Assume？

來源

2010-06-23 Dan Bryant

最新版本已啓用'ForAll'，你可能想試試:) – porges 2010-07-09 21:56:44

Code Contracts User Manual指出：「靜態合同檢查器尚未處理ForAll或Exists量子。」直到它，在我看來，選項是：

忽略警告。
在致電AddRequested()之前添加Contract.Assume(subGroup != null)。
在致電AddRequested()之前添加支票。也許if (subGroup == null) throw new InvalidOperationException()或if (subGroup != null) AddRequested(subGroup)。

選項1並沒有幫助。選項2是有風險的，因爲它會繞過AddRequested()需求合同，即使IUnboundTagGroup.GetAllGroups()不再確保後置條件。我會選擇3.

來源

2010-06-25 08:42:29

謝謝;我想我可能會使用Assume，因爲原始代碼（合同前）沒有空檢查。它也乾淨地標記了靜態證明者需要「幫助」的各個地方，以便希望我可以回過頭來移除其中的一些，因爲證明者變得更加強大。 – 2010-06-25 13:10:00

在代碼合同中使用Contract.ForAll

回答

相關問題