为什么我会收到由 C# 代码编写的格式错误的合同？

Question

当我在下面编写此合同时，Visual Studio 显示错误。

错误 20 方法“....get_Page”中的合同部分格式错误

是否是 if 块有问题？

public int? Page
{
  get
  {
    int? result = Contract.Result<int?>();

    if (result != null)
        Contract.Ensures(result >= 0);

    return default(int?);
  }
}

编辑：

Lasse V. Karisen 在评论中发表了：

怎么样：Contract.Ensures(result == null || result >= 0); ？

是的，Karisen，我之前已经尝试过并且可以编译。但问题仍然存在：使用合约时是否可以有 if ？

我遇到的另一个问题是无能为力的（主要考虑上面的示例），还涉及结果的使用：

public int IndexOf(T item)
{
    Contract.Assert(item != null);
    Contract.Assert((item as IEntity).ID > 0);

    int result = Contract.Result<int>();
    Contract.Ensures(result >= -1);

    return default(int);
}

Answer 1

合同格式错误，因为所有合同条款必须出现在任何其他代码之前。

Answer 2

您不需要 if 来进行布尔操作，而是使用暗示！

public int? Page
{
    get
    {
        Contract.Ensures( (result!= null).Implies(result >= 0) );
        var result = ...

        ...


        return result;
    }
}

此外，在测试方法参数和其他先决条件时，您应该使用 Requires not assert。

public int IndexOf(T item)
{
    Contract.Requires(item != null);
    Contract.Requires((item as IEntity).ID > 0);
...

Answer 3

只是有一个猜测。也许应该是Contract.Ensures(result.Value >= 0)？

Answer 4

所有 Ensures 和 Requires 调用必须位于方法或属性主体中的所有其他语句之前，这包括像您正在使用的有助于可读性的简单赋值。

正确的语法

public int? Page {
    get {
        Contract.Ensures(Contract.Result<int?>() == null 
            || Contract.Result<int?>() >= 0); 

        return default(int?);
        }
    }
 }

这是非常难看，比正常的if (x || y) throw new ArgumentOutOfRangeException()难看得多。

特殊属性

有一种迂回的方法可以解决这个问题。 ContractAbbreviatorAttribute 和 ContractArgumentValidatorAttribute 是 ccrewrite 可以理解的特殊属性，它们可以让您的生活更轻松。 （有关详细信息，请参阅系统.Diagnostics.Contracts MSDN 上的命名空间文档或代码合同 手动。）

如果使用 .NET 4 或更早版本：
这些属性位于 .NET 4.5 开始的框架中，但对于之前的版本，您可以从 Code Contracts 安装目录中获取它们的源文件。 (C:\Program Files (x86)\Microsoft\Contracts\Languages\) 在该文件夹中有 CSharp 和 VisualBasic 子文件夹，它们具有 < code>ContractExtensions.cs（或 .vb）包含所需代码的文件。

ContractAbbreviatorAttribute
此属性可以有效地让您创建合同宏。有了它，您的页面属性可以像这样编写：

public int? Page {
    get {
        EnsuresNullOrPositive();
        return default(int?)
    }
}

[ContractAbbreviator]
static void EnsuresNullOrPositive(int? x) {
    Contract.Ensures(
        Contract.Result<int?>() == null ||                 
        Contract.Result<int?>() >= 0);
}

EnsuresNullOrPositive 也可以保存在静态类中并在您的项目中重复使用，或者公开并放置在实用程序库中。您还可以使其更加通用，如下一个示例。

[ContractAbbreviator]
static void EnsuresNullOrPositive<Nullable<T>>(Nullable<T> obj) {
    Contract.Ensures(
        Contract.Result<Nullable<T>>() == null ||                 
        Contract.Result<Nullable<T>>() >= default(T));
}

对于我自己的实用程序库，我有一个名为 Requires 的静态类和一个名为 Ensures 的静态类，每个类都有许多用 ContractAbbreviator 修饰的静态方法。以下是一些示例：

public static class Requires {

    [ContractAbbreviator] 
    public static void NotNull(object obj) {  
        Contract.Requires<ArgumentNullException>(obj != null);
    }

    [ContractAbbreviator]
    public static void NotNullOrEmpty(string str) {
        Contract.Requires<ArgumentNullException>(!string.IsNullOrEmpty(str));
    }

    [ContractAbbreviator]
    public static void NotNullOrEmpty(IEnumerable<T> sequence) {
        Contract.Requires<ArgumentNullException>(sequence != null);
        Contract.Requires<ArgumentNullException>(sequence.Any());
    }
}

public static class Ensures {
    [ContractAbbreviator]
    public static void NotNull(){
        Contract.Ensures(Contract.Result<object>() != null);
    }
}

可以像这样使用：

public List<SentMessage> EmailAllFriends(Person p) {
    Requires.NotNull(p); //check if object is null
    Requires.NotNullOrEmpty(p.EmailAddress); //check if string property is null or empty
    Requires.NotNullOrEmpty(p.Friends); //check if sequence property is null or empty
    Ensures.NotNull(); //result object will not be null

    //Do stuff
}

ContractArgumentValidatorAttribute
我在教程之外没有使用过这个，但基本上它可以让您在单个调用中编写多个 if (test) throw new ArgumentException() 调用，其行为类似于对 Contract 的调用.需要。由于它只处理参数验证，因此对您的后置条件示例没有帮助。

Answer 5

合约上有条件编译标志。
在发布更多代码时

if condition
    contract
return

，

if condition
   return

您现在看到问题了吗？