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 に答える