List wrapper

Question

Hi,

I'm making a class wrapping a List<T>, for logging purposes. This results in 6 unproven contracts (ensures and requires). Is this a known issue, or am i doing something unsupported?

I can supply you with a sample file..

Regards,

Matthijs ter Woord

Answer 1

Could you please post the minimal amount of code to repro your situation?

---

while(!Asleep) sheep++;

Answer 2

The code is below. It gives an "ensures unproven" in the Add method.

Some notes about the code:
+ Some methods are implemented yet, but this makes no difference.
+ the mBackend field is readonly and assigned in constructor, so technically the Invariant shouldnt even be neccessary, but that's a different story...


Code:

public class WrappedCollection<T>: ICollection<T> {
        private readonly ICollection<T> mBackend = new List<T>();
        
        [ContractInvariantMethod]
        private void Invariant() {
            ICollection<T> @this = this;
            Contract.Invariant(mBackend != null);
        }
        void ICollection<T>.Add(T item) {
            mBackend.Add(item);
        }

        void ICollection<T>.Clear() {
            throw new NotImplementedException();
        }

        bool ICollection<T>.Contains(T item) {
            throw new NotImplementedException();
        }

        void ICollection<T>.CopyTo(T[] array, int arrayIndex) {
            throw new NotImplementedException();
        }

        int ICollection<T>.Count {
            get {
                return mBackend.Count;
            }
        }

        bool ICollection<T>.IsReadOnly {
            get {
                return false;
            }
        }

        bool ICollection<T>.Remove(T item) {
            return mBackend.Remove(item);
        }

        IEnumerator<T> IEnumerable<T>.GetEnumerator() {
            return mBackend.GetEnumerator();
        }

        System.Collections.IEnumerator System.Collections.IEnumerable.GetEnumerator() {
            return mBackend.GetEnumerator();
        }
    }

Answer 3

Thanks for reporting this. There's definitely something broken in the static checker. I'm investigating.

---

Cheers, -MaF (Manuel Fahndrich)