c# - 为什么我收到 'Invariant unproven' 警告

Question

我不明白这条消息想告诉我什么:

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);

Answer 1

我了解到的是，要向静态分析器证明正确性，您需要 checkin 代码，例如:

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 已被证明，并且在运行时，如果启用了运行时检查，它将验证它是否为真。

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

格雷格