标签: code-contracts

我最近偶然发现了Code Contracts,并开始在我的C#项目中使用它们.但是,我还有许多用C++/CLI编写的项目.

对于C#和VB,Code Contracts在项目属性对话框中提供了一个方便的配置面板.对于C++/CLI项目,没有这样的面板.

从文档,我得到的印象是添加代码契约到C++/CLI项目的支持应该是调用一些外部工具作为构建过程的一部分(即一个简单的问题ccrefgen.exe,cccheck.exe和ccrewrite.exe).但是,有关呼叫序列的命令行选项和限制的数量让我有点害怕.

任何人都能指出一种简单的方法来运行Code Contracts工具作为Visual Studio中构建过程的自动化部分吗？

如果我写这个:

public sealed class Foo
{
    private int count;
    private object owner;
    private void Bar()
    {
        Contract.Requires(count > 0);
        Contract.Ensures(owner == null || count > 0);

        if (count == 1)
            owner = null;
        --count;
    }
}

静态合同检查器可以证明所有断言.

但如果我写这个:

public sealed class Foo
{
    private int count;
    private object owner;
    private void Bar()
    {
        Contract.Requires(count > 0);
        Contract.Ensures(owner == null || count > 0);

        --count;
        if (count == 0)
            owner = null;
    }
}

它声称后置条件owner == null || count > …

我有以下代码:

class Program
{
    static void Main(string[] args)
    {
        Console.WriteLine(SqrtRoot(0));
        Console.WriteLine(SqrtRoot(10));
        Console.WriteLine(SqrtRoot(-10));
        Console.ReadKey();
    }

    public static int SqrtRoot(int i)
    {
        Contract.Requires(i >= 0);
        return (int)Math.Sqrt(i);
    }
}

我在调试模式下运行它,它应该在最后一行触发某种错误

Console.WriteLine(SqrtRoot(-10));

尽管如此,它还没有.它似乎忽略了Contract.Requires()调用.在尝试使用代码合同时,我应该设置一些东西吗？

我正在使用Visual Studio 2010 RC.

谢谢

我正在使用3.5库来进行微软代码合同

public object RetrieveById(int Id)
{    
    //stuff happens...
    Contract.Ensures(newObject != null, "object must not be null");
    return newProject;
    //No error message if I move the Contract.Ensures to here
    //But it isn't asserting/throwing a contract exception here either           
}

我得到编译器消息:"错误18方法'中的try块中的合同部分'Controller.RetrieveById(System.Int32)'

更新:

我在你的帮助下想出来了:

• 移到顶部

• 检查Contract.Result

  Contract.Ensures(Contract.Result()!= null,"object不能为null");

在我的项目中,静态检查被禁用,但是当我使用cmd运行msbuild.exe时,它会开始对每个项目进行静态检查...有没有办法,带参数来禁用它？

我只是在.Net 4.0中玩代码合同,并且必须缺少一些明显的东西,因为它们的行为并不像我期望的那样.

我总是使用一个简单的if ... then .. throw语句来在函数的开头执行任何验证.

if (hours < 0 || hours > 8)
    throw new ArgumentOutOfRangeException("hours", "Hours must be between 0 and 8");

我简单地用这个替换了

Contract.Requires<ArgumentOutOfRangeException>(hours >= 0 && hours <= 8, "Hours must be between 0 and 8");

但它似乎从未在我的单元测试中引发问题.

    public static DurationUnit HoursAsDuration(int hours)
    {
        Contract.Requires<ArgumentOutOfRangeException>(hours >= 0 && hours <= 8, "Hours must be between 0 and 8");

        switch (hours)
        {
            case 1:
            case 2:
                return DurationUnit.Quarter;
            case 3:
            case 4:
                return DurationUnit.Half;
            case 5:
            case 6: …

我不确定我在这里做错了什么,或者是否需要修复......

我有一个自定义的Dictionary包装类,这里是一段必要的代码片段.

public int Count
{
    get
    {
        Contract.Ensures(Contract.Result<int>() >= 0);

        return InternalDictionary.Count;
    }
}

public bool ContainsKey(TKey key)
{
    //This contract was suggested by the warning message, if I remove it
    //I still get the same warning...
    Contract.Ensures(!Contract.Result<bool>() || Count > 0);

    return InternalDictionary.ContainsKey(key);
}

唯一的原因,我添加了的containsKey行是因为我得到了下面的警告消息(现在仍然如此)Codecontracts: ensures unproven: !Contract.Result<bool>() || @this.Count > 0.我可以删除这一行并仍然得到相同的问题!

我该怎么做才能摆脱这些问题？

更新:

我也试过(按照建议)......

public Boolean ContainsKey(TKey key)
{
    Contract.Requires(Count == 0 || InternalDictionary.ContainsKey(key));
    Contract.Ensures(!Contract.Result<bool>() || Count > 0);

    return InternalDictionary.ContainsKey(key);
}

警告5方法'My.Collections.Generic.ReadOnlyDictionary …

在上图中,您可以看到代码合同中的警告.我不认为这是合法的,this永远不会null.

这是一个错误还是我错过了什么？

此属性是以下类的成员:

public class NHibernateIQueryableQueryBase<TEntity, TQuery, TQueryInterface>
    : IQuery<TEntity>, IFluentQueryInterface<TEntity, TQueryInterface>
    where TQuery : NHibernateIQueryableQueryBase<TEntity, TQuery,
                                                 TQueryInterface>,
                   TQueryInterface
    where TQueryInterface : IQuery<TEntity>

更新:
将属性更改为以下内容仍显示警告 - 在线return result;:

public TQueryInterface And
{
    get
    {
        var result = this as TQuery;
        return result;
    }
}

以下代码:

Contract.Requires<ArgumentException>(command != null, Resources.Messages.CommandNotSpecified);

电话

Contract.AssertMustUseRewriter (ContractFailureKind kind, System.String message)

如果您使用的是Visual Studio,这似乎是由于未将代码约定配置为使用运行时协定检查而导致的.

文章@ http://devjourney.com/blog/code-contracts-part-2-preconditions/暗示在没有配置运行时检查的情况下生成的代码是:

public static void Requires<TException>(bool condition)
where TException: Exception
{
    AssertMustUseRewriter(ContractFailureKind.Precondition, "Requires<TException>");
}

有没有人知道在MonoDevelop中做什么,以便合同按预期工作？

我得到的确切例外是:

2012-11-13 23:33:24.815 StickX[339:c07] mvx: Diagnostic:  34.46 Exception masked NotImplementedException: The requested feature is not implemented.
      at System.Environment.FailFast (System.String message) [0x00000] in /Developer/MonoTouch/Source/mono/mcs/class/corlib/System/Environment.cs:821 
  at System.Diagnostics.Contracts.Contract.AssertMustUseRewriter (ContractFailureKind kind, System.String message) [0x00011] in /Developer/MonoTouch/Source/mono/mcs/class/corlib/System.Diagnostics.Contracts/Contract.cs:83 
  at System.Diagnostics.Contracts.Contract.Requires[ArgumentException] (Boolean condition, System.String userMessage) [0x00000] in /Developer/MonoTouch/Source/mono/mcs/class/corlib/System.Diagnostics.Contracts/Contract.cs:271 

代码契约只是像处理任何其他变量那样处理任务,而不是异步地等待结果.因此,以下方案将不起作用,并导致合同异常,因为在方法返回时,它是一个不完整的任务,并且不会在该时间点设置结果.以下方案是否有任何合理的解决方法？

public Task LoadAppModel()
{
    Contract.Ensures(app.User != null);
    Contract.Ensures(app.Security != null);
    Contract.Ensures(app.LocalSettings != null);

    return Task.WhenAll(
        store.GetUserAsync().ContinueWith(t => { app.User = t.Result; }),
        store.GetSecurityAsync().ContinueWith(t => { app.Security = t.Result; }),
        store.GetLocalSettingsAsync().ContinueWith(t => { app.LocalSettings = t.Result; }));
}

任何建议,将不胜感激.:)我宁愿不打破合同模式.