标签: code-contracts

在Windows 7 x64上的VS2012中使用Code Contracts 1.4.51019.0时,我从ccrewrite收到以下编译错误: "该方法或操作未实施."

它似乎是由属性访问者和async缺乏内在的方法的组合引起的await.

复制步骤:

创建一个新的类库,启用"完整"运行时合同检查:

namespace CodeContractsAsyncBug
{
    using System.Threading.Tasks;

    public class Service
    {
        // Offending method!
        public async Task ProcessAsync(Entity entity)
        {
            var flag = entity.Flag;
        }
    }

    public class Entity
    {
        public bool Flag { get; set; }
    }
}

还有其他人经历过这个吗？

在REST世界中,我们有类似Swagger规范的东西,它完全描述了REST接口边界(客户端和服务器之间)的合同.这些Swagger规范可用于自动生成REST客户端,也可用于为REST API使用者自动生成文档.此外,这些Swagger规范也是CI和版本化API的宝贵资产.

我想知道异步发布订阅世界中是否存在类似的解决方案:让我们说一下RabbitMQ上的典型AMQP消费者/制作人....

最好的祝福,

巴特

从表面看,对象初始化器似乎对.net 4.0"代码契约"提出了问题,通常在对象构造函数完成时应该建立不变量.然而,据推测,对象初始化器需要在构造完成后设置属性.

我的问题是,"代码契约"的不变量是否能够处理对象初始化器,"好像"属性是在构造函数完成之前设置的？那确实非常好!!

我刚刚开始一个新的Web应用程序,我想在我的JavaScript中实现某种形式的contract'esque样式验证.我做了一些快速的谷歌搜索,并遇到了JsContact,但语法不是我想到的.有人知道其他图书馆吗？

我想我希望语法类似于

String.prototype.padLeft = function(c, width) {
  Verify.value(c).isRequired().isNotNull().isChar();
  Verify.value(width).isRequired().isNotNull().isNumber().greaterThan(0);

  ...

  Verify.value(result).isNotNull();

  return result;
};

虽然将我自己的库与我想要的语法/方法放在一起不会花费很长时间,但如果其他人已经完成了工作并且它足够接近,那么它将节省我一些时间.提前致谢.

UPDATE

我将没有时间在今天下午工作,所以我会再花几个小时来看看是否有人有任何建议.如果没有,我会发布我在某处创建的任何内容作为下面的答案供其他人参考,如果他们愿意的话.

我还考虑了一些有意义的API,我现在正在考虑像(人为的例子):

 function searchUser(firstName, middleInit, lastName) {
   Verify.value(firstName).isString().matching(/\w+/);       // Must have value
   Verify.value(middleInit).whenNotNull().isChar();          // May be null, but not undefined
   Verify.value(lastName).isString().withMinimumLengthOf(2); // Must have value

   ...
 }

 function syncTime(serverTime, now) {
   Verify.value(serverTime).isDate();         // Must have value.
   Verify.value(now).whenDefined().isDate();  // May be undefined, but not null.

 }

我当前的想法是容忍NULL或UNDEFINED值是非典型的(至少对我而言？),而不是显式指定值.isNotNull()你实际上会禁用.whenDefined()或.whenNotNull()的规则如上所示.我可能会在UNDEFINED上使.whenNotNull()没有错误,但我认为NULL与UNDEFINED是一个重要的区别; 我们会看到......所有其他方法都很典型......想法？评论？

我有一个基本的问题,可能是这么明显,但由于某种原因,我似乎无法成功安装和使用代码合同.

我从MSDN下载了软件包,按照在线文档安装了它,但我仍然收到以下代码语句的IDE警告:

Contract.Requires(inputParameter != "");

IDE警告是:

"跳过方法调用.编译器不会生成方法调用,因为该方法是有条件的,或者是没有实现的部分方法"

在启用代码合同的过程中我遗漏了什么？我正在使用VS2010 Ultimate SP1

我问这个问题,因为每当我尝试从Visual Studio 2010中的立即窗口调用扩展方法时,我都会收到以下错误:

System.Collections.Generic.IEnumerable'不包含'ToList'的定义,也没有扩展方法'ToList'接受类型'System.Collections.Generic.IEnumerable'的第一个参数(你是否缺少using指令或装配参考？)

如果立即窗口不支持扩展方法,那么为什么当我键入我的变量(类型IEnumerable<QueryFilter>)后跟一个点时,IntelliSense会列出所有扩展方法？

我在命令窗口中输入的内容没有任何问题,因为如果我将其复制并粘贴到我的代码文件中并运行,则可以正常工作.

使用Visual Studio 2012为同一解决方案做同样的事情工作正常.如果我切换回VS2010并且问题仍然存在.

我正在手工制作新代码.我想确保我不遗余力.

除了指定代码合同以指导Pex之外,我还能做些什么吗？所以它在数字密集型代码中产生了良好的覆盖范围？

尝试在http://research.microsoft.com/en-us/projects/pex/pexconcepts.pdf中搜索关键字"float"以获取一些背景信息.

浮点数的算术约束通过对有理数的转换来近似,并且在Z3之外使用启发式搜索技术来找到浮点约束的近似解.

...并且...

符号推理.Pex使用自动约束求解器来确定哪些值与测试和被测代码相关.但是,约束求解器的能力是,并且总是会受到限制.特别是,Z3不能精确地推理浮点运算.

或者,您是否知道.NET下的工具更适合在.NET下查找数字异常的任务？我知道http://fscheck.codeplex.com/但它不执行符号推理.

我有这个结构(简化为简洁):

public struct Period
{
    public Period(DateTime? start, DateTime? end) : this()
    {
        if (end.HasValue && start.HasValue && end.Value < start.Value)
        {
            throw new ArgumentOutOfRangeException("end", "...");
        }
        Contract.EndContractBlock();

        this.start = start;
        this.end = end;
    }

    private readonly DateTime? start;
    private readonly DateTime? end;

    public static Period operator +(Period p, TimeSpan t)
    {
        Contract.Assume(!p.start.HasValue || !p.end.HasValue || p.start.Value <= p.end.Value);
        return new Period(
            p.start.HasValue ? p.start.Value + t : (DateTime?) null,
            p.end.HasValue ? p.end.Value + t : (DateTime?) null);
    }
} …

在过去的几个月里,我一直在为我的公司开发一个辅助项目,但是现在已经决定它们在现有产品中是合适的.

我一直在使用微软的代码合同开发侧面项目进行静态类型检查(部分原因是我之前没有使用它们并且渴望学习).

我的问题是,如果我将代码签入到代码库中,并且所有其他开发人员都需要安装代码合同工具才能继续开发吗？我知道有一个事实,他们都没有安装它,我在这里是初级,所以我怀疑我能说服他们所有人接受它.

我正在使用.Net 4.5,因此包含了代码契约库,但我想知道Visual Studio是否会抱怨他们CONTRACTS_FULL每次构建时都没有使用构建选项中指定的构建,或者,如果我离开CONTRACTS_FULL在构建选项中,当另一个开发人员尝试构建时会发生什么？此外,我想知道当合同失败时最终产品将如何行动,但代码尚未使用代码合同重写器构建.

我只用一个项目创建了一个新的解决方案.创建了一个简单的函数,它触发了代码合同违规,卸载了代码契约CONTRACTS_FULL但未指定.构建并运行它并收到以下错误:

Run-time exception (line 8): An assembly (probably "hdxticim") must be rewritten using the code contracts binary rewriter (CCRewrite) because it is calling Contract.Requires<TException> and the CONTRACTS_FULL symbol is defined.  Remove any explicit definitions of the CONTRACTS_FULL symbol from your project and rebuild.  CCRewrite can be downloaded from http://go.microsoft.com/fwlink/?LinkID=169180. 
After the rewriter is installed, it can be enabled in Visual Studio from the project's Properties page on the …

静态检查有很多信息Contract.ForAll只有有限或没有支持.

我做了很多实验,发现它可以用于:

• Contract.ForAll(items, i => i != null)
• Contract.ForAll(items, p)哪里p是类型Predicate<T>

它不能用于:

• 现场访问
• 物业访问
• 方法组(我认为委托在这里被分配)
• 实例方法调用

我的问题是:

• 有哪些其他类型的代码ForAll可以使用？
• 代码合同是否经过Contract.ForAll(items, i => i != null)验证,以后在代码中从列表中取出一个项目(即通过索引)时,该项目不为空？

这是完整的测试代码:

public sealed class Test
{
    public bool Field;
    public static Predicate<Test> Predicate;

    [Pure]
    public bool Property
    {
        get { return Field; }
    }    

    [Pure]
    public static bool Method(Test t)
    {
        return t.Field;
    }

    [Pure]
    public bool InstanceMethod()
    {
        return Field; …