none
Problems with static checker and wrapper around generic list

    Question

  • I use the following class as wrapper around a generic list in order to
    to comply to the DoNotExposeGenericLists rule of FXCop:

    using System.Collections;
    using System.Collections.Generic;
    using System.Diagnostics.Contracts;
    
    namespace ContractOnListWrapper
    {
        public partial class StringCollection : ICollection<string>
        {
            private readonly List<string> list = new List<string>();
    
            public StringCollection()
            {
            }
    
            [Pure]
            public int Count
            {
                get
                {
                    Contract.Ensures(
                        Contract.Result<int>() == this.list.Count);
                    return this.list.Count;
                }
            }
    
            [Pure]
            public bool IsReadOnly
            {
                get { return false; }
            }
    
            [Pure]
            public string this[int index]
            {
                get
                {
                    Contract.Requires(index >= 0);
                    Contract.Requires(index < this.Count);
    
                    return this.list[index];
                }
            }
    
            public void Add(string item)
            {
                int oldCount = this.Count;
                this.list.Add(item);
                // without the following assertion:
                // " ensures unproven: this.Count == Contract.OldValue(this.Count) + 1"
                Contract.Assert(this.Count == oldCount + 1);
            }
    
            public void Clear()
            {
                this.list.Clear();
                // without the following assertion:
                // "ensures unproven: this.Count == 0"
                Contract.Assert(this.Count == 0);
            }
    
            [Pure]
            public bool Contains(string item)
            {
                bool result = this.list.Contains(item);
                // without the following assumption:
                // "ensures unproven: !Contract.Result<bool>() || this.Count > 0"
                Contract.Assume(!result || (this.Count > 0));
                return result;
            }
    
            public void CopyTo(string[] array, int arrayIndex)
            {
                // without the following assertion:
                // "requires unproven: arrayIndex + this.Count  <= array.Length"
                Contract.Assert(arrayIndex + this.Count <= array.Length);
                this.list.CopyTo(array, arrayIndex);
            }
    
            [Pure]
            public IEnumerator<string> GetEnumerator()
            {
                return this.list.GetEnumerator();
            }
    
            [Pure]
            IEnumerator IEnumerable.GetEnumerator()
            {
                return this.list.GetEnumerator();
            }
    
            [Pure]
            public int IndexOf(string item)
            {
                return this.list.IndexOf(item);
            }
    
            public void Insert(int index, string item)
            {
                Contract.Requires(index >= 0);
                this.list.Insert(index, item);
            }
    
            public bool Remove(string item)
            {
                return this.list.Remove(item);
            }
    
            public void RemoveAt(int index)
            {
                Contract.Requires(index >= 0);
                Contract.Requires(index < this.Count);
                this.list.RemoveAt(index); // V1.2.30312.0:
    // requires unproven: index < this.Count } [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(this.list != null); } } }

    The static checker (V1.2.30118.5) is able to prove the contracts (all options for implicit
    obligations are enabled), although the needed Contract.Assert statement are very obscure.
    The new version 1.2.30312.0 fails to prove all contracts and emits a warning in the
    RemoveAt method at the marked line. With the new version the assert statements are
    also necessary in order to get no warnings in the affected methods.
    Tuesday, March 16, 2010 4:29 PM

Answers

  • Thanks for trying. It is true that sometimes one has to help the checker by adding such assertions in order to break the problem into smaller manageable chunks. Since the assertions are themselves proven, you are not losing anything, except the effort to write them in your code.

    Clearly, we can always improve the checker, but just as clearly, there will always be cases where the programmer will need to help. No magic here.


    Cheers, -MaF (Manuel Fahndrich)
    Thursday, June 03, 2010 12:17 AM
    Owner

All replies

  • Hi,

    Just derive your custom collection from Collection<T> instead.  It will provide a valid implementation for you: No need to reimplement ICollection<T> and no need to keep your own private List<T>.

    Note that property gets are automatically assumed Pure so you don't have to mark them.

    - Dave
    http://davesexton.com/blog
    Wednesday, March 17, 2010 2:13 AM
  • Hi Dave,

    if I use Collection<T> instead, things become ugly when I need the methods of List<T>, like Sort, then
    one has to use a construct like this

    public StringCollection() : base(new List<string>())
    {
    }
    
    public string Sort()
    {
        List<string> items = (List<string>)Items;
        Contract.Assume(items != null);
        return items.Sort();
    }
    It would be better to fix the bugs in the static checker then to use such a walk around.
    Wednesday, March 17, 2010 6:44 AM
  • Hi,

    Hmm, having to write 3 lines of code is worse than having to write an entire custom implementation of ICollection<T>?  I'd have to disagree :)

    And what other examples of List<T> methods do you need other than Sort?  Remember, the LINQ methods that work on IEnumerable can be used with your custom Collection<T> and they'll provide all of the functionality that is built-in to List<T> without having to reinvent anything, with the exception of in-line sorting, as you've pointed out.

    Alternatively, just use the built-in StringCollection type instead:

      http://msdn.microsoft.com/en-us/library/system.collections.specialized.stringcollection.aspx

    Or don't use a custom collection at all, if all that you need is a List<string> anyway.  Getting around the FxCop warning is even simpler than implementing a custom collection:

    public IList<string> MyStringCollection
    {
      get { return myStrings; }
    }
    
    private readonly List<string> myStrings = new List<string>();
    
    public void SortMyStringCollection()
    {
      myStrings.Sort();
    }

    The idea behind the FxCop warning is simply that List<T> is not extensible, which makes versioning difficult.  Instead you should expose, preferably, an interface like IList<T>, ICollection<T> or IEnumerable<T>, depending upon the needs of the consumers of your class.  Alternatively, you can expose Collection<T> or a custom collection that derives from Collection<T>, because it's extensible, but I typically prefer the interface approach whenever possible because it doesn't get more extensible than that.

    --
    For what it's worth, I was able to reproduce the behavior that you've identified in your example code, and at least a couple of areas do seem like bugs to me as well.  The problem appears to be that the static checker is ignoring the stronger ensurances that you've added to your ICollection<string> implementation.

    For example, even adding Contract.Ensures(Contract.Result<int>() == 0) and then returning 0 in your Count implementation, the static checker still warns that Count == 0 is unproven in the implementation of the Clear method.

    - Dave
    http://davesexton.com/blog
    Wednesday, March 17, 2010 12:59 PM
  • Hi Dave,

    you are absolutely right with your proposed solutions,
    but it seems that you misunderstood my intentions
    of providing the code above: in my real code I have
    several different wrapper implementations around
    a List<T>, where T are several different own classes.
    Most wrapper classes provide only a very small set of methods
    and others provide an ICollection<T> interface
    (when the consumer code forced this).
    The above code was only a minimal testcase showing the different
    bugs in the static checker which I found in these
    different types of wrappers using the string class only as
    replacement of my own classes. Therefore it is clear that the
    provided code can be replaced by something much simpler as
    you correctly suggested.

    Alexander

    Wednesday, March 17, 2010 4:39 PM
  • Hi,

    I just tested the above code using the new version 1.3.30524.1. This new version can now prove all assertions if one changes the line "Contract.Assert(this.Count == oldCount + 1);" in the Add method to "Contract.Assert(this.Count >= oldCount);", but the use of the explicit assertions are still necessary in order to get no warnings.

    Alexander

    Thursday, May 27, 2010 7:56 AM
  • Thanks for trying. It is true that sometimes one has to help the checker by adding such assertions in order to break the problem into smaller manageable chunks. Since the assertions are themselves proven, you are not losing anything, except the effort to write them in your code.

    Clearly, we can always improve the checker, but just as clearly, there will always be cases where the programmer will need to help. No magic here.


    Cheers, -MaF (Manuel Fahndrich)
    Thursday, June 03, 2010 12:17 AM
    Owner
  • Hey, So I tried something a bit different.
    I added the following to my class

    Snippet

    Snippet
    [ContractInvariantMethod
    ]
    private void ObjectInvariant() {
        Contract .Invariant(Count >= 0);
    }

    This took care of the need to not add all the Asserts in the methods. I still had to have the Ensures on the Count though.

    Hope this helps some one.

    Raul


    Slacker.
    • Edited by Raul Rangel Wednesday, August 18, 2010 5:26 PM reformating code
    Wednesday, August 18, 2010 5:23 PM