标签: code-contracts

我试图在代码契约中展示不变量,我想我会给出一个排序的字符串列表的例子.它在内部维护一个数组,有额外的空间用于添加等 - 就像List<T>基本上一样.当它需要添加一个项目时,它会将它插入到数组中,等等.我想我有三个不变量:

• 计数必须合理:非负数,最多与缓冲区大小一样大
• 缓冲区未使用部分中的所有内容都应为null
• 缓冲区的已使用部分中的每个项目应至少与其前面的项目一样"大"

现在,我试图以这种方式实现它:

[ContractInvariantMethod]
private void ObjectInvariant()
{
    Contract.Invariant(count >= 0 && count <= buffer.Length);
    for (int i = count; i < buffer.Length; i++)
    {
        Contract.Invariant(buffer[i] == null);
    }
    for (int i = 1; i < count; i++)
    {
        Contract.Invariant(string.Compare(buffer[i], buffer[i - 1]) >= 0);
    }
}

不幸的是,ccrewrite搞乱了循环.

用户文档说该方法应该是一系列调用Contract.Invariant.我是否真的必须像这样重写代码？

Contract.Invariant(count >= 0 && count <= buffer.Length);
Contract.Invariant(Contract.ForAll
    (count, buffer.Length, i => buffer[i] == null));
Contract.Invariant(Contract.ForAll
    (1, count, i => string.Compare(buffer[i], …

可能重复:
如何配置Pex以尊重代码合同？

目前,当我运行pex探索时,我在我的类中创建的代码契约被视为pex探索结果中的错误.我想当你使用代码合同进行pex勘探时,合同失败应该被视为预期的行为.这是导致异常的代码.

测试方法:

[PexMethod]
public void TestEquality(Guid userId, string username, string password, string securityQuestion, string securityAnswer)
{
    UserSecurity user = UserTools.CreateUser(Guid.NewGuid(), username, password, securityQuestion, securityAnswer);

    bool passwordResult = UserTools.VerifyInput(password, user.Password, user.PasswordSalt);
    bool securityAnswerResult = UserTools.VerifyInput(securityAnswer, user.SecurityAnswer, user.SecurityAnswerSalt);

    Assert.IsTrue(passwordResult, "Password did not correctly re-hash");
    Assert.IsTrue(securityAnswerResult, "Security Answer did not correctly re-hash");
}

失败的方法调用:

public static UserSecurity CreateUser(Guid userId, string username, string password, string securityQuestion, string securityAnswer)
{
    Contract.Requires(userId != Guid.Empty);
    Contract.Requires(!string.IsNullOrWhiteSpace(username));
    Contract.Requires(!string.IsNullOrWhiteSpace(password));
    Contract.Requires(!string.IsNullOrWhiteSpace(securityQuestion));
    Contract.Requires(!string.IsNullOrWhiteSpace(securityAnswer));
    Contract.Ensures(Contract.Result<UserSecurity>() != null);

    byte[] passwordSalt;
    byte[] …

我想知道,如何在.NET Core中正确使用Code Contracts ,到目前为止我试图将CC添加到我的项目中,进行编译和调试.我对每个使用的呼叫中出现的消息Contract.Requires以及通过Google搜索找到的信息感到困惑.

消息说明:

必须使用代码契约二进制重写器(CCRewrite)重写程序集,因为它正在调用Contract.Requires<TException>并且CONTRACTS_FULL符号已定义.CONTRACTS_FULL从项目中删除符号的任何显式定义并重建.CCRewrite ....

正如我所看到的,项目属性中没有CC选项,因为我可以看到CC的Github存储库几乎已经死了.是如何在.NET Core中成功使用CC的？

如果没有,是否有任何简单的方法来替换它们？我用Contract.Requires和ContractClassAttribute.更换Contract.Requires是显而易见的,但ContractClassAttribute让我大吃一惊:-)

Pure方法如下？我会这样说,因为它不会改变当前的类,因此,在运行此方法之前,我们现在可以在类中"看到"的所有内容在之后仍然完全相同.我对么？

class Set {
    ...
    public ISet<T> UnionWith(ISet<T> set) {
       ISet<T> unionSet = ...

        foreach (Element element in this) {
            unionSet.Add(element);
        }

        foreach (Element element in set) {
           unionSet.Add(element);
        }

        return unionSet;
    }
}

我可能会说我对Code Contracts非常熟悉:我已经阅读并理解了大部分用户手册,并且已经使用了很长一段时间了,但我仍然有疑问.当我搜索SO代码"未经证实的代码合同"时,有很多点击,都在问为什么他们的具体陈述无法被静态证明.虽然我可以做同样的事情并发布我的具体情况(这是顺便说一句:

)

我更愿意理解为什么任何代码合同条件可以或不可以证明.有时我对它能证明的东西印象深刻,有时我......嗯......礼貌地说:绝对没有留下深刻的印象.如果我想了解这一点,我想知道静态检查器使用的机制.我相信我会从经验中学习,但我会在Contract.Assume所有地方喷洒语句以使警告消失,我觉得这不是Code Contracts的意思.谷歌搜索没有帮助我,所以我想问你们你们的经历:你们看到了什么(不明显的)模式？是什么让你看到光明？

在组合使用代码分析和代码合同时,我会收到很多警告

CA1062:Microsoft.Design:在外部可见方法'Foo.Bar(Log)'中,在使用之前验证参数'log'.

在Foo.Bar,我有一份验证的合同log.

public Bar(Log log)
{
   Contract.Requires(log != null);
   log.Lines.Add(...);
   // ...
}

有没有办法让FxCop理解代码合约？

我有以下场景:

public interface ISomething
{
    void DoStuff();
    //...
}

public class Something : ISomething
{
    private readonly ISomethingElse _somethingElse;
    //...

    public Something (ISomethingElse somethingElse)
    {
         Contract.Requires(somethingElse != null);
        _somethingElse = somethingElse;
    }

    public void DoStuff()
    {
        // *1* Please look at explanation / question below
        _somethingElse.DoThings();
    }
 }

在第1行并且打开静态检查器时,我会收到一条警告,说明_somethingElse可能为空,如果我添加合同,它会给我错误

[Type]实现接口方法{Interface.Method}因此无法添加需求

这里最好的事情是什么？我看到的选项包括

1. 一个保护条款,虽然看起来有点极端
2. 一个 Contract.Assume
3. 一个我没想过的隐藏的第三个选项

请注意readonly,在构造函数中设置值后,该字段是如此,因此无法更改.因此,代码合同的警告似乎有点无关紧要.

我想问你的问题很广泛但同时它非常具体.首先,我必须说,我最感兴趣的是适用于.net环境的答案.

好吧,我想提高我生成的代码级别.现在我主要使用TDD和静态代码分析来确保我的代码是正确的.最近我听了Dino Esposito关于代码合同的演讲,现在我想将它与其他技术结合使用.在听Dino的同时我也回忆起了Debug.Assert()和Trace.Assert().

具体来说,我会问几个问题:

• 我应该如何编写合同和单元测试以相互补充？
• 我应该只在每种方法或公共方法中使用代码合同吗？
• 我应该阻止使用Debug.Assert()吗？什么时候可以使用它们？(例如,请注意.net中的不变量仅在公共方法/属性出口处进行检查.那么,通过简单方法在方法中间进行一些检查是否可以Assert()？)
• 你能否推荐我一个开源项目,所有这些技术都被正确使用,因为一张图片描绘了千言万语？

我最近在我的办公室里听到过关于.Net"合同"的一些讨论,然而,当我问我的一些同事时,他们不能轻易地向我解释他们的用途,甚至是什么.

有没有人有任何资源,解释,也许还有他们使用的教程？

谢谢,

保罗

我想在我的代码库中开始使用代码契约.

我已经使用了代码分析,启用了所有规则,并且目标是零警告.

但是,在使用时,Contract.Requires(parameter != null)我收到代码分析的警告,即CA1062:

CA1062:Microsoft.Design:在外部可见的方法"富",用它之前验证参数"参数".

这很不幸,我不想禁用该规则,因为我发现它很有用.但我也不想压制它的每一个错误发生.

有解决方案吗？