代码契约[类型]实现了接口的方法{} Interface.Method因此不能添加要求 [英] Code Contracts [Type]implements interface method {Interface.Method} thus cannot add requires

问题描述

我有以下情形：

 公共接口ISomething 
 {
无效DoStuff（）; 
 // ... 
} 
 
公共类的东西：ISomething 
 {
私人只读ISomethingElse _somethingElse; 
 // ... 
 
公共的东西（ISomethingElse somethingElse）
 {
 Contract.Requires（somethingElse！= NULL）; 
 _somethingElse = somethingElse; 
} 
 
公共无效DoStuff（）
 {
 // * 1 *请看看下面
 _somethingElse.DoThings解释/问题（）; 
} 
} 
  

目前行的 1 的和与静态检查，我会得到一个警告说， _somethingElse 可能是空的，如果我添加了一个合同，它会给我的错误

[类型]实现了接口的方法{} Interface.Method因此不能添加要求

什么是在这里做的最好的事情？选择我看到包括

1. 保护条款，但它似乎是一个
   有点极端


2. 在 Contract.Assume


3. 是我没有想到的

隐藏的第三个选项



请注意该字段是只读所以在构造设定值后，不可能发生变化。因此，从代码合同警告似乎的位的无关紧要。




解决方案

说明





第3部分：合同继承 规定所有先决条件必须在根的方法来定义的用户手册继承/实现连锁：








如果一个客户端可以确保他们满足的前提和具有可变 0 的静态类型为 T ，那么客户端不应该得到的一个先决条件违反时，他们叫 OM 。这需要真实的，即使运行值 0 的类型 U 。因此，该方法 UM 不能添加一个前提条件，即比 TM 的前提强。





虽然我们可以允许一个较弱的先决条件，我们已经发现，这样做的并发症得不偿失。只是我们还没有看到任何令人信服的例子，弱化的前提是很有用的。因此，我们不允许在一个亚型添加任何前提条件的。





因此​​，方法的前提条件必须在继承/实现链的根法，即宣布，第一个虚拟或抽象方法声明，或接口方法本身。






解决方案





在您的情况，最好的行动当然是要建立一个不变，指出 _somethingElse 字段不能为null：

  [ContractInvariantMethod] 
私人无效ObjectInvariant（）{
 Contract.Invariant（_somethingElse！= NULL）; 
} 
  

这是当然总是正确的，因为外地被标记只读并在构造函数初始化。静态检查是不是能够推断出，虽然这对自己，所以你必须明确地告诉它通过不变的。





您可以选择添加一个后置条件 Contract.Ensures（_somethingElse！= NULL）; 来你的构造，但静态检查并不需要它。


。

I have the following scenario:

public interface ISomething
{
    void DoStuff();
    //...
}

public class Something : ISomething
{
    private readonly ISomethingElse _somethingElse;
    //...

    public Something (ISomethingElse somethingElse)
    {
         Contract.Requires(somethingElse != null);
        _somethingElse = somethingElse;
    }

    public void DoStuff()
    {
        // *1* Please look at explanation / question below
        _somethingElse.DoThings();
    }
 }

At line 1 and with the static checker on, I'll get a warning saying that _somethingElse is possibly null, and if I add a contract it will give me the error

[Type]implements interface method {Interface.Method} thus cannot add requires

What's the best thing to do here? Options I see include

1. a guard clause, though it seems a bit extreme
2. a Contract.Assume
3. a hidden third option that I haven't thought of

Please note the field is readonly so after setting the value in the constructor it is not possible to change. Thus, the warning from code contracts seems a bit irrelevant.

解决方案

Explanation

Section 3: Contract Inheritance of the user manual states that all preconditions must be defined in the root method of an inheritance/implementation chain:

If a client makes sure that they have satisfied the precondition and has a variable o whose static type is T, then the client should not get a precondition violation when they call o.M. This needs to be true even if the runtime value o has type U. Therefore, the method U.M cannot add a precondition that is stronger than the precondition of T.M.

While we could allow a weaker precondition, we have found that the complications of doing so outweigh the benefits. We just haven't seen any compelling examples where weakening the precondition is useful. So we do not allow adding any preconditions at all in a subtype.

As a consequence, method preconditions must be declared on the root method of an inheritance/implementation chain, i.e., the first virtual or abstract method declaration, or the interface method itself.

Solution

In your situation, the best course of action is to set up an invariant stating that the _somethingElse field is never null:

[ContractInvariantMethod]
private void ObjectInvariant() {
    Contract.Invariant(_somethingElse != null);
}

This is of course always true, as the field is marked readonly and initialised in the constructor. The static checker isn't able to infer this on its own though, so you must explicitly tell it through that invariant.

You can optionally add a postcondition Contract.Ensures(_somethingElse != null); to your constructor, but the static checker doesn't require it.

这篇关于代码契约[类型]实现了接口的方法{} Interface.Method因此不能添加要求的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！