2

我不明白这条消息试图告诉我什么：

CodeContracts: invariant unproven: _uiRoot != null && _uiRoot.Children != null && _uiRoot.RowDefinitions != null && _uiRoot.ColumnDefinitions != null

这是方法：

private void AddRowToGrid(List<UIElement> row) {

        Contract.Requires(row != null);

        _uiRoot.RowDefinitions.Add(new RowDefinition());
        VerifyColumnCount(row.Count);

        int colunmn = 0;
        foreach (UIElement uiElement in row.Where(element => element != null))
        {
            if (uiElement != null)
            {
                uiElement.SetValue(Grid.ColumnProperty, colunmn++);
                if (_uiRoot.RowDefinitions != null)
                {
                    uiElement.SetValue(Grid.RowProperty, _uiRoot.RowDefinitions.Count - 1);
                    if (_uiRoot.Children != null)
                    {
                        _uiRoot.Children.Add(uiElement);
                    }
                }
            }
        }
    }

这是不变量：

[ContractInvariantMethod]
    private void ObjectInvariant() {
        Contract.Invariant(_layoutList != null && this._layoutList.DefaultLayoutItemEntities != null);
        Contract.Invariant(_uiRoot != null && _uiRoot.Children != null && _uiRoot.RowDefinitions != null &&
                           _uiRoot.ColumnDefinitions != null);
        Contract.Invariant(_dragDropManager != null);
    }

我尝试添加以下 Contract.Ensures，但它仍然给我同样的信息：

 Contract.Ensures(_uiRoot != null && _uiRoot.Children != null && _uiRoot.RowDefinitions != null &&
                         _uiRoot.ColumnDefinitions != null);
4

1 回答 1

1

我学到的是，要证明静态分析器的正确性，您需要检查代码，例如：

if(_uiRoot == null || _uiRoot.Children == null || _uiRoot.RowDefinitions == null ||
                     _uiRoot.ColumnDefinitions == null)
      throw new Exception();

分析器将看到这一点并确定这是 Contact.Ensures 的证明。

另一种选择是使用：

Contract.Assume(_uiRoot != null && _uiRoot.Children != null && _uiRoot.RowDefinitions != null &&
                     _uiRoot.ColumnDefinitions != null);

这将告诉分析器 Contract.Ensure 已被证明，并且在运行时，如果启用运行时检查，它将验证它是否为真。

更好的是编写代码，以便分析器可以通过分析代码本身来证明。对我来说，这就是代码契约的最大好处——代码证明了自己，因为它写得很好。

格雷格

于 2013-06-13T21:30:08.627 回答