在代码合约中使用 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 需要一个非空输入参数（它实现了一个具有 Requires 契约的接口），因此我在传递到 AddRequested 的子组上收到“requires unproven: group != null”错误。我是否正确使用了 ForAll 语法？如果是这样，并且求解器根本不理解，是否有另一种方法可以帮助求解器识别合同，或者我只需要在调用 GetAllGroups() 时使用假设？
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?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
代码合同用户手册指出，“静态合同检查器不会尚未处理 ForAll 或 Exists 量词。”在此之前，在我看来，选项是：
AddRequested()之前添加Contract.Assume(subGroup != null)。AddRequested()之前添加检查。也许if（子组或== null) throw new InvalidOperationException()
if (subGroup != null)。AddRequested(子组)
选项 1 并没有真正的帮助。选项 2 存在风险，因为即使
IUnboundTagGroup.GetAllGroups()不再确保后置条件，它也会绕过AddRequested()Requires 契约。我会选择选项 3。The Code Contracts User Manual states, "The static contract checker does not yet deal with quantiers ForAll or Exists." Until it does, it seems to me the options are:
Contract.Assume(subGroup != null)before the call toAddRequested().AddRequested(). Maybeif (subGroupor== null) throw new InvalidOperationException()
if (subGroup != null).AddRequested(subGroup)
Option 1 doesn't really help. Option 2 is risky because it will circumvent the
AddRequested()Requires contract even ifIUnboundTagGroup.GetAllGroups()no longer ensures that post-condition. I'd go with option 3.