Okay, I have yet another Code Contracts question. I have a contract on an interface method that looks like this (other methods omitted for clarity):
[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;
}
}
I have code consuming the interface that looks like this:
public void AddRequested(IUnboundTagGroup group)
{
foreach (IUnboundTagGroup subGroup in group.GetAllGroups())
{
AddRequested(subGroup);
}
//Other stuff omitted
}
AddRequested
requires a non-null input parameter (it implements an interface which has a Requires contract) and so I get a 'requires unproven: group != null' error on the subGroup being passed into AddRequested
. Am I using the ForAll syntax correctly? If so and the solver simply isn't understanding, is there another way to help the solver recognize the contract or do I simply need to use an Assume whenever GetAllGroups() is called?