为什么我得到'不变式未证明'警告

本文关键字：证明 警告 不变式 为什么 | 更新日期: 2023-09-27 18:18:21

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

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(_uiRoot != null && _uiRoot.Children != null && _uiRoot.RowDefinitions != null &&
                         _uiRoot.ColumnDefinitions != null);

为什么我得到'不变式未证明'警告

我所学到的是，为了向静态分析器证明正确性，您需要有一个检入代码，例如:

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

分析器将看到这个并决定这是contact . ensure的证明。

另一个选项是使用:

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

这将告诉分析器契约。确保已被证明，并且，在运行时，如果启用了运行时检查，它将验证它是否为真。

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

格雷格

相关文章：