c# - 为什么我在 C# 代码中得到格式错误的合同？

Question

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

Error 20 Malformed contract section in method '....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但是问题仍然存在：在使用合约时是不是可以有s ？

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

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（有关详细信息，请参阅System.Diagnostics.ContractsMSDN 上的命名空间文档或代码合同手册。）

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

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
}

ContractArgumentValidatorAttributeif (test) throw new ArgumentException()我没有在教程之外使用过这个，但基本上它允许您在一个调用中 编写多个调用，其行为类似于对Contract.Requires. 由于它仅处理参数验证，因此对您的后置条件示例没有帮助。

Answer 5

合同上有条件编译标志。在发布更多你的代码

if condition
    contract
return

变成

if condition
   return

你现在看到问题了吗？