破碎建议确保简单分配 [英] Broken suggested ensures for simple assignment

问题描述

你好，

我是CC的新手，并试图在本周末试一试。花了一些时间后，我开始理解它，并能够使用它。但是，我遇到了一些问题。

首先，我在看似简单的案例中遇到了建议 - 这表明非常合同我已经拥有：

 public class TestClass {public TestClass（）{//导致建议确保：//消息2 CodeContracts：建议确保：Contract.Ensures（ this.Count == 12）; C：\ Users\censored\src\ContractTest \TestClass.cs 8 ContractTest Contract.Ensures（this.Count == 12）; this.Count = 12; public int Count {get;私人集; public void Init（）{//导致建议确保：//消息1 CodeContracts：建议确保：Contract.Ensures（this.Count == 11）; C：\ Users\censored\src\ContractTest \TestClass.cs 25 ContractTest Contract.Ensures（this.Count == 11）; this.Count = 11; } [ContractInvariantMethod] private void Invariants（）{Contract.Invariant（this.Count> = 0）;在上面的例子中，我得到的唯一输出是我的评论中指出的两个，加上"Checked 11 assertions：11 correct"。我提出这个问题是因为我的下一个问题似乎表明合同提取存在问题.. 
 
 
在下面的例子中，它没有证明我的保险，即使很少有变化。发生了什么？
公共类TestClass {private object [] redHerring; public TestClass（）{Contract.Ensures（this.Count == 12）; //确保未经证实：this.Count == 12 TestClass.cs 17 Contract.Ensures（this.redHerring！= null）; this.Count = 12; this.redHerring =新对象[1]; public int Count {get;私人集; public void Init（）{Contract.Ensures（this.Count == 11）; this.Count = 11; } [ContractInvariantMethod] private void Invariants（）{Contract.Invariant（this.Count> = 0）; Contract.Invariant（this.redHerring！= null）; } 
 
 
 
这会导致以下输出：
 
 
 
 
 
 
 
 
 
 
 
 
 
 
建议确保：合约.Ensures（this.Count == 11）;  TestClass.cs  25 
 
建议确保：Contract.Ensures（this.Count == 12）;  TestClass.cs  10 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
建议确保：Contract.Ensures（this.redHerring.Length == 1）;  TestClass.cs  10 
 
 
确保未经证实：this.Count == 12  TestClass.cs  17 
 
 
消息  8  CodeContracts：已检查17个断言：16个正确1个未知
 
 
 
 
 
因为我已经声明了一个数组初始化（我在Count init之后做了），它无法证明Count设置得当吗？
 
 
 
 
 
 
 
 
 
 
 
 
 
 
我正在使用Visual Studio 2010，CC 1.4.60317.12，Mode = Standard，警告级别= hi，推断和建议一切。
解决方案
 
 
 Egh，我应该意识到这一点。花了一个周末试图解决这个问题，我在这里发布后半小时就得到了它。
 
 
 
 
 
保险不会持有，因为数组初始化可能抛出OutOfMemoryException，在这种情况下，分析器似乎不愿意对类的状态做任何保证。 
 
 
 
好吧，那么处理这个问题的正确方法是什么？在我的实际代码中，这可以防止验证者在其操作时能够更多地证明其余的类。如果构造函数抛出异常，任何消费者都不会对
那个特定对象有任何追索权，如果有的话，只能选择退出，尝试清理一些内存，并尝试重新分配一个新的宾语。同时，我班上的其他人都无法证明，因为它有几个内存分配实例。
 
 
 
 
 
我还是不喜欢知道为什么它的建议确保我已经有了。
 
 
 
Howdy,

I'm new to CC, and tried to give it a go this weekend. After having spent some time with it, i'm starting to understand it and be able to use it. However, I'm having some problems.

First, I'm having trouble with the suggestions in seemingly simple cases - it's suggesting the very contract I already have:
    public class TestClass    {        public TestClass()        {            // Causes a suggested ensures:            // Message	2	CodeContracts: Suggested ensures: Contract.Ensures(this.Count == 12);	C:\Users\censored\src\ContractTest\TestClass.cs	8	ContractTest            Contract.Ensures( this.Count == 12 );            this.Count = 12;        }        public int Count { get; private set; }        public void Init()        {            // Causes a suggested ensures:            // Message	1	CodeContracts: Suggested ensures: Contract.Ensures(this.Count == 11);	C:\Users\censored\src\ContractTest\TestClass.cs	25	ContractTest            Contract.Ensures( this.Count == 11 );                        this.Count = 11;        }        [ContractInvariantMethod]        private void Invariants()        {            Contract.Invariant( this.Count >= 0 );        }    }
In the above case, the only outputs I get are the two indicated in my comments, plus "Checked 11 assertions: 11 correct". I bring this up because it seems like my next problem is indicating a problem with contract extraction..
In the following case, it's failing to prove my Ensures, even though very little has changed. What's going on?
    public class TestClass    {        private object[] redHerring;        public TestClass()        {            Contract.Ensures( this.Count == 12 ); // ensures unproven: this.Count == 12 TestClass.cs 17                        Contract.Ensures( this.redHerring != null );            this.Count = 12;            this.redHerring = new object[1];        }        public int Count { get; private set; }        public void Init()        {            Contract.Ensures( this.Count == 11 );                        this.Count = 11;        }        [ContractInvariantMethod]        private void Invariants()        {            Contract.Invariant( this.Count >= 0 );            Contract.Invariant( this.redHerring != null );        }    }

This causes the following outputs:




Suggested ensures: Contract.Ensures(this.Count == 11); TestClass.cs 25

Suggested ensures: Contract.Ensures(this.Count == 12); TestClass.cs 10 






Suggested ensures: Contract.Ensures(this.redHerring.Length == 1); TestClass.cs 10
ensures unproven: this.Count == 12 TestClass.cs 17
Message 8 CodeContracts: Checked 17 assertions: 16 correct 1 unknown

Just because I've declared an array initialization (that i'm doing after the Count init), it can't prove that Count is set properly?




I'm using Visual Studio 2010, CC 1.4.60317.12, Mode = Standard, Warning level = hi, infer and suggest for everything.
解决方案
Egh, I should've realized this. Spent a weekend trying to figure it out and I get it half an hour after posting on here..

The Ensures doesn't hold because the array initialization could throw an OutOfMemoryException, in which case, it seems, the analyzer is unwilling to make any guarentees about the state of the class.

Alright, so what's the right way to deal with this? In my actual code, this prevents the verifier from being able to prove more about the rest of the class as its operated. If the constructor throws an exception, any consumer wouldn't have any recourse for
 that particular object and, if anything, would only have the option to back off, try to clean up some memory, and try to reallocate a new object. Meanwhile, the rest of my class can't be proven out, because it has a couple instances of memory allocation.

I still don't know why its suggesting Ensures that I already have, though.


                        
这篇关于破碎建议确保简单分配的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！