7

我正在尝试lock使用以下示例来确定 .NET 代码合同如何与关键字交互：

public class TestClass
{
  private object o1 = new object();
  private object o2 = new object();

  private void Test()
  {
    Contract.Requires(this.o1 != null);
    Contract.Requires(this.o2 != null);
    Contract.Ensures(this.o1 != null);

    lock (this.o2) {
      this.o1 = new object();
    }
  }
}

当我运行 Code Contract 静态分析工具时，它会打印一条警告：Ensures unproven: this.o1 != null

如果我这样做：

  • 更改为, o2_locko1
  • 将块o1内部更改为,locko2
  • lock在块内添加第二行，将 a 分配new object给o2
  • 更改lock (this.o2)为if (this.o2 != null),
  • 完全删除该lock语句。

警告消失。

但是，将lock块内的行更改为var temp = new object();（从而o1从方法中删除所有引用）仍然会导致警告：

private void Test()
  {
    Contract.Requires(this.o1 != null);
    Contract.Requires(this.o2 != null);
    Contract.Ensures(this.o1 != null);

    lock (this.o2) {
      var temp = new object();
    }
  }

所以有两个问题：

  1. 为什么会出现此警告？
  2. 可以做些什么来防止它（记住这是一个玩具示例，lock实际代码中实际上发生了一些事情）？
4

2 回答 2

2

下面是静态检查器如何处理锁和不变量：

如果您使用 lock(x.foo) { ... } 形式锁定某些内容，静态检查器会将 x.foo 视为 x 的保护锁。在锁定范围的末尾，它假定其他线程可能访问 x 并对其进行修改。结果，静态检查器假定 x 的所有字段只满足锁定范围后的对象不变量，仅此而已。

请注意，这并没有考虑所有线程交错，只是在锁定范围末尾的交错。

于 2013-04-24T21:31:57.170 回答
1

将以下代码添加到您的类中：

    [ContractInvariantMethod]
    private void ObjectInvariants()
    {
        Contract.Invariant(o1 != null);
    }

我无法告诉你为什么，但在这种情况下，静态验证器似乎确实考虑了私有字段分配并且缺少修改它的方法作为该字段不会被修改的充分证据。这可能是验证程序中的错误？可能值得在Code Contracts 论坛上报告。

于 2013-04-24T07:06:55.323 回答