c# – 代码合同：我们必须在委托方法中冗余地指定Contract.Requi

我认为代码示例值得一千字：

public bool CrushGodzilla(string weapon,int velocity)
    {
        Contract.Requires(weapon != null);

        // long code

        return false;
    }

    public bool CrushGodzilla(string weapon)
    {
        Contract.Requires(weapon != null);   // specify contract requirement here
                                             // as well???

        return this.CrushGodzilla(weapon,int.MaxValue);
    }

对于运行时检查,这并不重要,因为我们最终总是会遇到需求检查,如果失败,我们会收到错误.

但是,当我们再次在第二次重载中未指定合同要求时,是否认为是不良做法？

此外,还将编译时间检查功能,也可能设计代码合同的时间检查.它似乎尚未在Visual Studio 2010中使用C#,但我认为有一些语言,如Spec#已经做了.当我们编写代码来调用这样的方法时,这些引擎可能会给我们提示,我们的参数当前可以是或将为null.

所以我想知道这些引擎是否会始终分析一个调用堆栈,直到找到一个当前不满足的合同的方法？

此外,here I learned about the difference between Contract.Requires(...) and Contract.Assume(...).我想这个差异也是在这个问题的背景下考虑的呢？