更多关于不变的未经证实和属性

问题描述

再次问好。关于证明不变量的另一个问题。假设您有以下课程：

公共课X {
  public X（String a）{
    Contract.Requires（！String.IsNullOrEmpty（a））;
    Contract.Ensures（A == a）; //或者我应该使用A！= null ???     _a =  a;
  }
  private String _a;
  [ContractInvariantMethod]   private void Invariants（）{
    Contract.Invariant（！String.IsNullOrEmpty（））;
  }
  public String A {
  得到{  return _a; }
  集合{
     Contract.Requires（！String.IsNullOrEmpty（value））;
     _a = a;
   }
 当我在该代码上运行静态解析器时，我最终得到了一个不变的未经证实的警告。我已经尝试将Contract.Ensures添加到setter但它只在添加 之后才有用一个Contract.Assume在_a = a之后;现在，当我看到这个小例子时，我的印象是，Contract.Ensures应该足以使一切正常，但似乎我错了。任何人都可以对此发表评论吗？

我注意到的另一件事是我必须复制我的代码才能进行静态分析。例如，当我看这个简单的例子时，我仍然不确定为什么我需要在构造函数上使用require，然后在不变量中复制它。我的意思是，说一个特定的属性不能为空是不是很难，对吧？

谢谢。

---

Luis Abreu

Hello again. One more question regarding proving invariants. Suppose that you have the following class:

public class X{
  public X(String a){
    Contract.Requires( !String.IsNullOrEmpty(a));
    Contract.Ensures( A == a); //or should I use A!=null???
    _a = a;
  }
  private String _a;
  [ContractInvariantMethod]
  private void Invariants(){
    Contract.Invariant( !String.IsNullOrEmpty() );
  }
  public String A{
   get{ return _a; }
   set{
     Contract.Requires( !String.IsNullOrEmpty(value));
     _a = a;
   }
  }
}

When I run the static parser over that code, I've ended up with an invariant unproven warning. I've tried adding Contract.Ensures to the setter but it only worked after adding  a Contract.Assume after the _a=a; instruction.

Now, When I look at this small example, I'm really under the impression that Contract.Ensures should be enough for making everything work, but it seems like I'm wrong. Can anyone comment on this?

Another thing I've noticed is that I've had to duplicate my code so that static analysis works. For instance, when I look at this simple example, I'm still not sure on why I need to use requires on the constructor and then duplicate that in invariants. I mean, it shouldn't be so hard to say that a specific property can't be null, right?

thanks.

---

Luis Abreu

推荐答案

您的示例（修复了下面的拼写）通过静态检查器就好了。你得到了什么问题？也许这取决于我们内部已有的修复。

your example (fixed for spelling below) passes the static checker just fine. What problel are you getting? Maybe that is dependent on a fix that we already have internally.

  public class X
  {
    public X(String a)
    {
      Contract.Requires(!String.IsNullOrEmpty(a));
      Contract.Ensures(A == a); //or should I use A!=null???
      _a = a;
    }
    private String _a;
    [ContractInvariantMethod]
    private void Invariants()
    {
      Contract.Invariant(!String.IsNullOrEmpty(_a));
    }
    public String A
    {
      get { return _a; }
      set
      {
        Contract.Requires(!String.IsNullOrEmpty(value));
        _a = value;
      }
    }
  }

 

这篇关于更多关于不变的未经证实和属性的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！