Issue with Static Extension Method

Question

I'm getting a couple of related warnings that I don't understand:

1> Window.xaml.cs(96,21,96,82): warning : CodeContracts: requires unproven: column >= 0 && column < grid.ColumnDefinitions.Count

1> WpfExtensions.cs(36,13,36,70): warning : CodeContracts: location related to previous warning

The code for Window looks like this:

[Conditional("DEBUG"), 
SuppressMessage("Microsoft.Performance", "CA1822:MarkMembersAsStatic")]
private void DisplayDebugGridLines(MouseButtonEventArgs e)
{
#if DEBUG
    if (e.ChangedButton == MouseButton.Right && Keyboard.IsKeyDown(Key.LeftCtrl | Key.LeftShift))
    {
        _mainGrid.ShowGridLines = !_mainGrid.ShowGridLines;

        for (int i = 0; i < _mainGrid.RowDefinitions.Count; i++)
        {
            if (_mainGrid.ShowGridLines)
                    {
            var uiElement = _mainGrid.GetElements<UIElement>(i, 0);

            if ((uiElement.Count > 0) && (uiElement[0].Visibility != Visibility.Collapsed))
            {

The second parameter to the _mainGrid.GetElements<UIElement>() call is what it is complaining about.  Here's the static extension method:

        [SuppressMessage("Microsoft.Design", "CA1062:Validate arguments of public methods", MessageId = "0", Justification = "CodeAnalysis doesn't fully get Code Contracts yet.")]
        public static Collection<TElement> GetElements<TElement>(this Grid grid, int row, int column) where TElement : UIElement
        {
            if (grid == null) throw new ArgumentNullException("grid");
            if (row < 0 || row >= grid.RowDefinitions.Count) 
                throw new ArgumentOutOfRangeException("row", row, @"Must be >= 0 and < " + grid.RowDefinitions.Count);
            if (column < 0 || column >= grid.ColumnDefinitions.Count) 
                throw new ArgumentOutOfRangeException("column", column, @"Must be >= 0 and < " + grid.ColumnDefinitions.Count);
            Contract.EndContractBlock();

            var elements = from UIElement element in grid.Children 
                           where element is TElement && Grid.GetRow(element) == row && Grid.GetColumn(element) == column 
                           select element as TElement; 

            return new Collection<TElement>(elements.ToList());
        }

AFAICT 0 is always a valid value for the Count property of ColumnDefinitions.  I tried putting the 0 in a variable and did a Contract.Assume(column >= 0 && column < _mainGrid.ColumnDefinitions.Count) but that didn't get rid of the warning. Is there another way to eliminate the warning (or fix the code if there's a bug here I'm not seeing)?

 

Answer 1

Hi Keith,

Your contract requires: column < grid.ColumnDefinitions.Count

And it's true that Grid.ColumnDefinitions returns ColumnDefinitionCollection, which implements ICollection<T>.Count, which ensures the return value is >= 0.

Therefore, it's possible that Grid.ColumnDefinitions.Count == 0; however, you're passing in 0 for column, which violates your contract: column < grid.ColumnDefinitions.Count.

In other words, GetElements assumes that: Grid.ColumnDefinitions.Count > 0

If you make this a requirement, then you'll have to prove it before calling GetElements, perhaps with an explicit assumption.

Even if you don't make it an explicit requirement, try adding the following assumption before calling GetElements:  

Contract.Assume(_mainGrid.ColumnDefinitions.Count > 0);

- Dave

---

http://davesexton.com/blog