标签: code-contracts

我说的是那些最终将在.NET 4.0中出现的代码契约.他们使用什么二进制重写器来注入使其全部工作并且公开可用的代码？我希望它不仅仅是一个编译器,因为我希望能够将它们的二进制重写器用于AOP.

因此,Visual Studio 2010的属性中似乎应该有一个"代码约定"选项卡.我找不到任何地方.也许这是我的Visual Studio安装的问题？我正在运行RC版本.

这就是我所拥有的:

替代文字http://img192.imageshack.us/img192/5928/lcmitpm2aur5e4uiabdtofw.png

谁知道什么可能是错的？也许我在找错了地方？

谢谢

我在C#中有一个商业应用程序,有单元测试.我可以使用NModel或Spec Explorer来提高可靠性并减少我的测试时间和费用吗？或者,如果我要用F#(甚至是Haskell)重写它,我可以看到哪种类型(如果有的话)的可靠性增加？

代码合同？ASML？

我意识到这是主观的,可能是议论性的,所以如果可能的话,请用数据备份你的答案.:)或者也许是一个有用的例子,比如埃里克埃文斯货运系统？

如果我们考虑

单元测试是特定的和强定理,在特定的"有趣实例"上准静态检查,类型是一般但弱定理(通常是静态检查),并且是一般和强定理的契约,动态检查在发生期间发生的特定实例正常的程序操作.(来自B. Pierce的类型被认为是有害的),

这些其他工具在哪里适合？

我们可以使用Java PathFinder,Scala等为Java提出类似的问题.

我刚开始使用.NET代码契约,我有一个像这样的保护条款

if (!file.Exists(path)) throw FileNotFoundException();

并替换为

Contract.Requires(File.Exists(path));

我不确定这是否正确,因为合同将处理I/O问题,但不确定这是否是一个问题.

基本上问题是:使用合同确保I/O问题(或外部/非单元问题)是否有任何问题？

我已经看到它写在其他地方SO,虽然企业库验证应用程序块旨在验证用户输入,代码契约旨在防止程序员错误.你会支持这个意见吗？为什么？

我的主要问题是如何处理我抛出的异常？

例如:

 Contract.Requires(foo != null);

如何在函数调用的uper级别中执行此抛出的异常？

我应该忽略它,当我看到它知道我的设计有问题并修复它时？

但是如果我在没有Contracts的情况下进行部署会发生什么呢？我会得到一个foo == null的参数,而且我的逻辑不知道如何处理这样的参数.然后一切都会崩溃.

有人可以解释如何处理所有这些情况吗？

谢谢

这是接口的合同类的一部分.

[Pure]
public bool IsDirty() {
    throw new NotImplementedException();
}

public void Save() {
    Contract.Ensures(!this.IsDirty()); //WARNING
    throw new NotImplementedException();
}

它正在产生这个警告:

警告CC1036:CodeContracts:在方法'EntityObjectContract.Save'的合同中检测到没有[Pure]的方法'IEntityObject.IsDirty'的调用.

......即使该Pure属性存在.我试过重建,重新打开Visual Studio,但每次都有相同的结果.知道怎么摆脱这个警告吗？我错过了什么吗？

我有以下代码片段:

    public static string returnString()
    {
        string[] stringList = { "a" };

        if (stringList.Count() != 1)
        {
            throw new Exception("Multiple values in list");
        }

        var returnValue = stringList.Single();

        Contract.Assert(returnValue != null, "returnValue is null");

        return returnValue;
    }

CodeContract说:

CodeContracts:断言未经证实.你是否在静态检查器不知道的Single上做了一些假设？

在我的理解中,Single()永远不会返回null - 它返回IEnumerable的唯一值或者抛出异常.如何向代码分析器证明这一点？

我从原始站点安装了代码合同,并尝试编写一些示例代码.但R#只是写道Method invocation is skipped.当我看反编译的源时,我看到该方法是有条件的:CONTRACTS_FULL必须定义常量.我检查Code Contracts了项目设置中选项卡中的所有内容,但似乎无法正常工作.

怎么修好？

我刚刚安装了Microsoft Code Contracts.它是.NET Framework和Visual Studio插件的一部分.它提供运行时检查和定义合同的静态检查.

该工具有四个警告级别,所以我设置最高.

我已经宣布了违反Liskov替代原则的课程.

public class Person
{
    protected int Age { get; set; }

    public Person(int age)
    {
        Contract.Requires(age > 0);
        Contract.Requires(age < 130);
        this.Age = age;
    }
}

public class Child : Person
{
    public Child(int age) : base(age)
    {
        Contract.Requires(age > 0); 
        Contract.Requires(age < Consts.AgeOfMajority);
        Contract.Requires(age < 130);
        this.Age = age;
    }
}

public static class Consts
{
    public readonly static int AgeOfMajority = 18;
}

LSP声明:

如果S是T的子类型,那么类型T的对象可以用类型S的对象替换而不改变该程序的任何所需属性

在我的例子中,违规将是这个对齐:Person person = new Child(23); …