标签: microsoft-contracts

有没有办法向ReSharper表明由于按合同设计需要检查,不会出现空引用？例如,以下代码将Possible 'null' assignment to entity marked with 'NotNull' attribute在第7行和第8行的ReSharper中引发warning():

private Dictionary<string, string> _Lookup = new Dictionary<string, string>();

public void Foo(string s)
{
    Contract.Requires(!String.IsNullOrEmpty(s));

    if (_Lookup.ContainsKey(s))
        _Lookup.Remove(s);
}

真正奇怪的是,如果删除该Contract.Requires(...)行,ReSharper消息就会消失.

更新

我通过ExternalAnnotations找到了解决方案,Mike也在下面提到过.以下是如何在Microsoft.Contracts中为函数执行此操作的示例:

• 创建一个Microsoft.Contracts在ExternalAnnotationsReSharper目录下调用的目录.
• 接下来,创建一个名为的文件Microsoft.Contracts.xml并填充如下:

<assembly name="Microsoft.Contracts">
    <member name="M:System.Diagnostics.Contracts.Contract.Requires(System.Boolean)">
        <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/>
        <parameter name="condition">
            <attribute ctor="M:JetBrains.Annotations.AssertionConditionAttribute.#ctor(JetBrains.Annotations.AssertionConditionType)">
                <argument>0</argument>
            </attribute>
        </parameter>
    </member>
</assembly>

• 重新启动Visual Studio,消息就消失了!

微软最近在DevLabs上发布了他们的Code Contracts框架并获得了商业许可.我们有兴趣在我们的项目中使用它们(主要是C#,一些C++/CLI)来逐步替换所有自定义验证代码,但我很想知道其他人在我们承诺之前使用它的经验,特别:

• 您是否认为该框架对于大型复杂的商业项目而言已经足够成熟？

• 使用它时遇到了什么问题？

• 你从中得到了什么好处？

• 它目前是否比它的价值更痛苦？

我意识到这是一个有点主观的问题,因为它需要意见,但鉴于这个框架是.NET 4.0的一个非常重要的部分,并且(可能)改变了我们编写验证代码的方式,我希望这个问题将会留下开放以收集有关该主题的经验,以帮助我做出具体的,可回答的问题的决定:

我们下个月应该开始使用吗？

请注意,我们不提供代码API,只提供Web服务,因此对于抛出异常类型方面的大多数代码打破兼容性并不是一个问题.然而,正如我希望更多人而不仅仅是我将受益于这篇文章及其答案,这个领域的任何细节都非常受欢迎.

例如,本文介绍了它们.

有什么好处？

静态分析似乎很酷,但同时它会阻止在单元测试中传递null作为参数的能力.(如果您按照文章中的示例进行操作)

关于单元测试的主题 - 如果您已经实施自动化测试,那么现在肯定没有任何关系可以代码合同吗？

更新

玩过代码合约后,我有点失望.例如,根据接受的答案中的代码:

public double CalculateTotal(Order order)
{
    Contract.Requires(order != null);
    Contract.Ensures(Contract.Result<double>() >= 0);
    return 2.0;
}

对于单元测试,您仍然必须编写测试以确保无法传递null,并且如果契约是业务逻辑,则结果大于或等于零.换句话说,如果我要删除第一个合同,除非我特意测试了这个功能,否则没有测试会中断.这是基于不使用内置于Visual Studio的更好(终极等)版本中的静态分析.

从本质上讲,它们都归结为编写传统if语句的另一种方式.我实际使用TDD的经验,代码合同显示了原因,以及我如何去做.

考虑以下两段代码:

    public static Time Parse(string value)
    {
        string regXExpres = 
           "^([0-9]|[0-1][0-9]|2[0-3]):([0-9]|[0-5][0-9])$|^24:(0|00)$";
        Contract.Requires(value != null);
        Contract.Requires(new Regex(regXExpres).IsMatch(value));
        string[] tokens = value.Split(':');
        int hour = Convert.ToInt32(tokens[0], CultureInfo.InvariantCulture);
        int minute = Convert.ToInt32(tokens[1], CultureInfo.InvariantCulture);
        return new Time(hour, minute);
    }

和

    public static Time Parse(string value)
    {
        if (value == null)
        {
            throw new ArgumentNullException("value");
        }
        string[] tokens = value.Split(':');
        if (tokens.Length != 2)
        {
            throw new FormatException("value must be h:m");
        }
        int hour = Convert.ToInt32(tokens[0], CultureInfo.InvariantCulture);
        if (!(0 <= hour && hour <= 24)) …

以下代码在前置条件下失败.这是代码合同中的错误吗？

static class Program
{
    static void Main()
    {
        foreach (var s in Test(3))
        {
            Console.WriteLine(s);
        }
    }

    static IEnumerable<int>Test (int i)
    {
        Contract.Requires(i > 0);
        for (int j = 0; j < i; j++)
            yield return j;
    }
}

我目前在ASP.NET MVC应用程序中使用Microsoft Code Contracts没有任何问题,但我似乎无法在基本的ASP.NET网站上运行它.我不完全确定它是用于这种类型的项目(虽然它应该没关系)所以我想把它带给每个人.

我可以很好地编译合同,但代码跳过它们,因为我假设它没有通过属性页面启用,就像你在其他项目类型(即ASP.NET MVC)中那样.我已经进入了我的ASP.NET网站中的项目的属性页面(它显示了一个对话框,而不是典型的属性页面),但它没有产生相同的菜单选项,因此,没有专门的部分编码合同.

此外,我在类库项目中正确启用了Microsoft Code Contracts,我将其用于将业务逻辑与Web站点分离.合同编译正常,但是当合同被违反时,它会抛出一个"Exception of type 'System.ExecutionEngineException' was thrown"没有内部异常的无法提供的错误.我的合同指定了一条在违规时显示的消息,但它不在异常范围内.它只是暂停了进程的执行(我认为这是Microsoft Code Contracts的默认功能).

我找不到任何明确说明特定项目类型可以或不可以(或不应该)与合同一起使用的地方,所以我只是想知道是否有人遇到过这个问题.

谢谢你的帮助!

当我在Visual Studio(2008)内部注意到静态验证警告时,我只是在Stack Overflow上回答某人的问题:

string[] source = { "1", "A", "B" };
var sourceObjects = Array.ConvertAll(source, c => new Source(c)).ToArray();

我收到消息需要未经证实的来源!= null.我觉得很明显,事实并非如此.这只是一个例子.另一方面,一些相当漂亮的东西似乎运作得相当好.

我正在使用1.2.20518.12版本(5月18日).我发现代码合同非常有趣,但有没有其他人有这样的案例？您是否认为当前的实现在实践中可用,或者您认为它们在这一点上纯粹是学术性的？

我把它做成了一个社区维基,但我想听听一些意见:)

我在下面编写此合同时显示错误.

错误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); ？

是卡里森,我之前尝试过这个并编译.但问题仍然存在:在使用合同时是不是可能有ifs？

我遇到的另一个问题是无能为力(主要考虑上面的例子),还涉及结果的使用:

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);
}

如何指示方法永远不会返回null？目前这是我的代码.

第19行获得了一个Ensures未经验证的消息,即使CreateFunction假定结果不是什么.

1         <Pure()> Public Function CreateFunction(Of TArg1, TArg2, TResult)(ByVal body As Func(Of Expression, Expression, BinaryExpression)) As Func(Of TArg1, TArg2, TResult)   
2             Contract.RequiresAlways(body IsNot Nothing)   
3             Contract.Assume(Contract.Result(Of Func(Of TArg1, TArg2, TResult))() IsNot Nothing)   
4   
5             Dim arg1 = Expression.Parameter(GetType(Integer), "arg1")   
6             Dim arg2 = Expression.Parameter(GetType(Integer), "arg2")   
7   
8   
9             Dim temp = Expression.Lambda(body(arg1, arg2), arg1, arg2)   
10             Contract.Assume(temp IsNot Nothing)   
11             Return DirectCast(temp.Compile, Global.System.Func(Of TArg1, TArg2, TResult))   
12         End Function  
13   
14         <Pure()> Public Function Add() As Func(Of T, T, …